Documentation

Mathlib.RingTheory.LocalRing.RingHom.Basic

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] :
@[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] :

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_isLocalRing {R : Type u_4} {S : Type u_5} [CommSemiring 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.

@[deprecated RingHom.domain_isLocalRing]
theorem RingHom.domain_localRing {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :

Alias of RingHom.domain_isLocalRing.


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.

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 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) :

If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

Every ring hom f : K →+* R from a division ring K to a nontrivial ring R is a local ring hom.

@[deprecated IsLocalRing.local_hom_TFAE]

Alias of IsLocalRing.local_hom_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

@[deprecated IsLocalRing.of_surjective]
theorem LocalRing.of_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S) [IsLocalHom f] (hf : Function.Surjective f) :

Alias of IsLocalRing.of_surjective.

@[deprecated IsLocalRing.surjective_units_map_of_local_ringHom]

Alias of IsLocalRing.surjective_units_map_of_local_ringHom.


If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

theorem RingEquiv.isLocalRing {A : Type u_4} {B : Type u_5} [CommSemiring A] [IsLocalRing A] [CommSemiring B] (e : A ≃+* B) :
@[deprecated RingEquiv.isLocalRing]
theorem RingEquiv.localRing {A : Type u_4} {B : Type u_5} [CommSemiring A] [IsLocalRing A] [CommSemiring B] (e : A ≃+* B) :

Alias of RingEquiv.isLocalRing.