Local rings homomorphisms #
We prove basic properties of local rings homomorphisms.
@[deprecated isLocalHom_id]
Alias of isLocalHom_id.
theorem
isLocalHom_toRingHom
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
{F : Type u_4}
[FunLike F R S]
[RingHomClass F R S]
(f : F)
[IsLocalHom f]
:
IsLocalHom ↑f
@[deprecated isLocalHom_toRingHom]
theorem
isLocalRingHom_toRingHom
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
{F : Type u_4}
[FunLike F R S]
[RingHomClass F R S]
(f : F)
[IsLocalHom f]
:
IsLocalHom ↑f
Alias of isLocalHom_toRingHom.
theorem
RingHom.isLocalHom_comp
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[Semiring R]
[Semiring S]
[Semiring T]
(g : S →+* T)
(f : R →+* S)
[IsLocalHom g]
[IsLocalHom f]
:
IsLocalHom (g.comp f)
@[deprecated RingHom.isLocalHom_comp]
theorem
RingHom.isLocalRingHom_comp
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[Semiring R]
[Semiring S]
[Semiring T]
(g : S →+* T)
(f : R →+* S)
[IsLocalHom g]
[IsLocalHom f]
:
IsLocalHom (g.comp f)
Alias of RingHom.isLocalHom_comp.
theorem
isLocalHom_of_comp
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[Semiring R]
[Semiring S]
[Semiring T]
(f : R →+* S)
(g : S →+* T)
[IsLocalHom (g.comp f)]
:
@[deprecated isLocalHom_of_comp]
theorem
isLocalRingHom_of_comp
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[Semiring R]
[Semiring S]
[Semiring T]
(f : R →+* S)
(g : S →+* T)
[IsLocalHom (g.comp f)]
:
Alias of isLocalHom_of_comp.
theorem
RingHom.domain_localRing
{R : Type u_4}
{S : Type u_5}
[CommSemiring R]
[CommSemiring S]
[H : LocalRing S]
(f : R →+* S)
[IsLocalHom f]
:
If f : R →+* S is a local ring hom, then R is a local ring if S is.
theorem
map_nonunit
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[LocalRing R]
[CommSemiring S]
[LocalRing S]
(f : R →+* S)
[IsLocalHom f]
(a : R)
(h : a ∈ LocalRing.maximalIdeal R)
:
f a ∈ LocalRing.maximalIdeal S
The image of the maximal ideal of the source is contained within the maximal ideal of the target.
theorem
LocalRing.local_hom_TFAE
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[LocalRing R]
[CommSemiring S]
[LocalRing S]
(f : R →+* S)
:
[IsLocalHom f, ⇑f '' ↑(LocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(LocalRing.maximalIdeal S),
Ideal.map f (LocalRing.maximalIdeal R) ≤ LocalRing.maximalIdeal S,
LocalRing.maximalIdeal R ≤ Ideal.comap f (LocalRing.maximalIdeal S),
Ideal.comap f (LocalRing.maximalIdeal S) = LocalRing.maximalIdeal R].TFAE
A ring homomorphism between local rings is a local ring hom iff it reflects units, i.e. any preimage of a unit is still a unit. https://stacks.math.columbia.edu/tag/07BJ
theorem
LocalRing.of_surjective
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[LocalRing R]
[CommSemiring S]
[Nontrivial S]
(f : R →+* S)
[IsLocalHom f]
(hf : Function.Surjective ⇑f)
:
theorem
LocalRing.surjective_units_map_of_local_ringHom
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
(h : IsLocalHom f)
:
Function.Surjective ⇑(Units.map ↑f)
If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.
@[instance 100]
instance
LocalRing.instIsLocalHomRingHomOfNontrivial
{K : Type u_4}
{R : Type u_5}
[DivisionRing K]
[CommRing R]
[Nontrivial R]
(f : K →+* R)
:
Every ring hom f : K →+* R from a division ring K to a nontrivial ring R is a
local ring hom.
Equations
- ⋯ = ⋯
theorem
RingEquiv.localRing
{A : Type u_4}
{B : Type u_5}
[CommSemiring A]
[LocalRing A]
[CommSemiring B]
(e : A ≃+* B)
: