Local rings homomorphisms #
We prove basic properties of local rings homomorphisms.
@[instance 100]
instance
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
instance
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)
theorem
RingHom.domain_isLocalRing
{R : Type u_4}
{S : Type u_5}
[Semiring R]
[CommSemiring S]
[IsLocalRing 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]
[IsLocalRing R]
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
[IsLocalHom f]
(a : R)
(h : a ∈ IsLocalRing.maximalIdeal R)
:
The image of the maximal ideal of the source is contained within the maximal ideal of the target.
theorem
IsLocalRing.local_hom_TFAE
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[IsLocalRing R]
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
:
[IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = 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.
theorem
IsLocalRing.of_surjective
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[IsLocalRing R]
[Semiring S]
[Nontrivial S]
(f : R →+* S)
[IsLocalHom f]
(hf : Function.Surjective ⇑f)
:
theorem
IsLocalHom.of_surjective
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Nontrivial S]
[IsLocalRing R]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
theorem
Function.Surjective.isLocalHom
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Nontrivial S]
[IsLocalRing R]
(f : R →+* S)
(hf : Surjective ⇑f)
:
Alias of IsLocalHom.of_surjective.
theorem
IsLocalRing.surjective_units_map_of_local_ringHom
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring 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
IsLocalRing.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.
theorem
RingEquiv.isLocalRing
{A : Type u_4}
{B : Type u_5}
[CommSemiring A]
[IsLocalRing A]
[Semiring B]
(e : A ≃+* B)
: