Documentation

Mathlib.RingTheory.LocalRing.RingHom.Defs

Local rings homomorphisms #

We Define local ring homomorhpisms.

Main definitions #

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

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.

Instances
    theorem IsLocalRingHom.map_nonunit {R : Type u_1} {S : Type u_2} :
    ∀ {inst : Semiring R} {inst_1 : 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.