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_1} {S : Type u_2} [Semiring R] [Semiring 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) ⊆ ↑(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.maximalIdeal_comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
theorem IsLocalRing.map_maximalIdeal_le {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
theorem IsLocalRing.map_maximalIdeal_lt_top {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
theorem IsLocalRing.of_surjective {R : Type u_1} {S : Type u_2} [Semiring 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 IsLocalRing.map_maximalIdeal_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
@[simp]
theorem IsLocalRing.map_ringEquiv_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
theorem RingEquiv.isLocalRing {A : Type u_4} {B : Type u_5} [Semiring A] [IsLocalRing A] [Semiring B] (e : A ≃+* B) :
instance instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial {R : Type u_4} [CommRing R] [IsLocalRing R] {n : ℕ} [Nontrivial (ZMod n)] (f : R →+* ZMod n) :