Local rings homomorphisms

We Define local ring homomorhpisms.

Main definitions

• IsLocalRingHom: A predicate on semiring homomorphisms, requiring that it maps nonunits to nonunits. For local rings, this means that the image of the unique maximal ideal is again contained in the unique maximal ideal.

class IsLocalRingHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) : Prop

A local ring homomorphism is a homomorphism f between local rings such that a in the domain is a unit if f a is a unit for any a. See LocalRing.local_hom_TFAE for other equivalent definitions.

• map_nonunit : ∀ (a : R), IsUnit (f a) → IsUnit a

  A local ring homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.

theorem IsLocalRingHom.map_nonunit {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} [self : IsLocalRingHom f] (a : R) : IsUnit (f a) → IsUnit a

A local ring homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.