Documentation

Mathlib.RingTheory.LocalRing.RingHom.Basic

Local rings homomorphisms #

We prove basic properties of local rings homomorphisms.

source
instance isLocalRingHom_id (R : Type u_4) [Semiring R] :
IsLocalRingHom (RingHom.id R)
Equations
  • ⋯ = ⋯
source
@[simp]
theorem isUnit_map_iff {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) :
IsUnit (f a) ↔ IsUnit a
source
@[simp]
theorem map_mem_nonunits_iff {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) :
f a ∈ nonunits S ↔ a ∈ nonunits R
source
instance 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) [IsLocalRingHom g] [IsLocalRingHom f] :
IsLocalRingHom (g.comp f)
Equations
  • ⋯ = ⋯
source
instance isLocalRingHom_equiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R ≃+* S) :
IsLocalRingHom ↑f
Equations
  • ⋯ = ⋯
source
@[simp]
theorem isUnit_of_map_unit {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) (h : IsUnit (f a)) :
IsUnit a
source
theorem of_irreducible_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) [h : IsLocalRingHom f] {x : R} (hfx : Irreducible (f x)) :
Irreducible x
source
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) [IsLocalRingHom (g.comp f)] :
IsLocalRingHom f
source
theorem RingHom.domain_localRing {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [H : LocalRing S] (f : R →+* S) [IsLocalRingHom f] :
LocalRing R

If f : R →+* S is a local ring hom, then R is a local ring if S is.

source
theorem map_nonunit {R : Type u_1} {S : Type u_2} [CommSemiring R] [LocalRing R] [CommSemiring S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] (a : R) (h : a ∈ LocalRing.maximalIdeal R) :
f a ∈ LocalRing.maximalIdeal S

The image of the maximal ideal of the source is contained within the maximal ideal of the target.

source
theorem LocalRing.local_hom_TFAE {R : Type u_1} {S : Type u_2} [CommSemiring R] [LocalRing R] [CommSemiring S] [LocalRing S] (f : R →+* S) :
[IsLocalRingHom f, ⇑f '' ↑(LocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(LocalRing.maximalIdeal S), Ideal.map f (LocalRing.maximalIdeal R) ≤ LocalRing.maximalIdeal S, LocalRing.maximalIdeal R ≤ Ideal.comap f (LocalRing.maximalIdeal S), Ideal.comap f (LocalRing.maximalIdeal S) = LocalRing.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. https://stacks.math.columbia.edu/tag/07BJ

source
theorem LocalRing.of_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [LocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S) [IsLocalRingHom f] (hf : Function.Surjective ⇑f) :
LocalRing S
source
theorem LocalRing.surjective_units_map_of_local_ringHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (h : IsLocalRingHom f) :
Function.Surjective ⇑(Units.map ↑f)

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

source
@[instance 100]
instance LocalRing.instIsLocalRingHomOfNontrivial {K : Type u_4} {R : Type u_5} [DivisionRing K] [CommRing R] [Nontrivial R] (f : K →+* R) :
IsLocalRingHom f

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

Equations
  • ⋯ = ⋯
source
theorem RingEquiv.localRing {A : Type u_4} {B : Type u_5} [CommSemiring A] [LocalRing A] [CommSemiring B] (e : A ≃+* B) :
LocalRing B