Local rings

Define local rings as commutative rings having a unique maximal ideal.

Main definitions

• LocalRing: A predicate on commutative semirings, stating that for any pair of elements that adds up to 1, one of them is a unit. This is shown to be equivalent to the condition that there exists a unique maximal ideal.
• LocalRing.maximalIdeal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.
• 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.
• LocalRing.ResidueField: The quotient of a local ring by its maximal ideal.

class LocalRing (R : Type u) [Semiring R] extends Nontrivial : Prop

A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1. Note that LocalRing is a predicate.

• of_is_unit_or_is_unit_of_add_one :: (
• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b

  in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.

• )

theorem LocalRing.isUnit_or_isUnit_of_add_one {R : Type u} [Semiring R] [self : LocalRing R] {a : R} {b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b

in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.

theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) : LocalRing R

theorem LocalRing.of_nonunits_add {R : Type u} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) : LocalRing R

A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

theorem LocalRing.of_unique_max_ideal {R : Type u} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) : LocalRing R

A semiring is local if it has a unique maximal ideal.

theorem LocalRing.of_unique_nonzero_prime {R : Type u} [CommSemiring R] (h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) : LocalRing R

theorem LocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u} [CommSemiring R] [LocalRing R] {a : R} {b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b

theorem LocalRing.nonunits_add {R : Type u} [CommSemiring R] [LocalRing R] {a : R} {b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R

def LocalRing.maximalIdeal (R : Type u) [CommSemiring R] [LocalRing R] : Ideal R

The ideal of elements that are not units.

Equations

• LocalRing.maximalIdeal R = { carrier := nonunits R, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

instance LocalRing.maximalIdeal.isMaximal (R : Type u) [CommSemiring R] [LocalRing R] : (LocalRing.maximalIdeal R).IsMaximal

Equations

• ⋯ = ⋯

theorem LocalRing.maximal_ideal_unique (R : Type u) [CommSemiring R] [LocalRing R] : ∃! I : Ideal R, I.IsMaximal

theorem LocalRing.eq_maximalIdeal {R : Type u} [CommSemiring R] [LocalRing R] {I : Ideal R} (hI : I.IsMaximal) : I = LocalRing.maximalIdeal R

theorem LocalRing.le_maximalIdeal {R : Type u} [CommSemiring R] [LocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) : J ≤ LocalRing.maximalIdeal R

@[simp]

theorem LocalRing.mem_maximalIdeal {R : Type u} [CommSemiring R] [LocalRing R] (x : R) : x ∈ LocalRing.maximalIdeal R ↔ x ∈ nonunits R

theorem LocalRing.isField_iff_maximalIdeal_eq {R : Type u} [CommSemiring R] [LocalRing R] : IsField R ↔ LocalRing.maximalIdeal R = ⊥

theorem LocalRing.of_isUnit_or_isUnit_one_sub_self {R : Type u} [CommRing R] [Nontrivial R] (h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) : LocalRing R

theorem LocalRing.isUnit_or_isUnit_one_sub_self {R : Type u} [CommRing R] [LocalRing R] (a : R) : IsUnit a ∨ IsUnit (1 - a)

theorem LocalRing.isUnit_of_mem_nonunits_one_sub_self {R : Type u} [CommRing R] [LocalRing R] (a : R) (h : 1 - a ∈ nonunits R) : IsUnit a

theorem LocalRing.isUnit_one_sub_self_of_mem_nonunits {R : Type u} [CommRing R] [LocalRing R] (a : R) (h : a ∈ nonunits R) : IsUnit (1 - a)

theorem LocalRing.of_surjective' {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective ⇑f) : LocalRing S

theorem LocalRing.maximalIdeal_le_jacobson {R : Type u} [CommRing R] [LocalRing R] (I : Ideal R) : LocalRing.maximalIdeal R ≤ I.jacobson

theorem LocalRing.jacobson_eq_maximalIdeal {R : Type u} [CommRing R] [LocalRing R] (I : Ideal R) (h : I ≠ ⊤) : I.jacobson = LocalRing.maximalIdeal R

class IsLocalRingHom {R : Type u} {S : Type v} [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} {S : Type v} [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.

instance isLocalRingHom_id (R : Type u_1) [Semiring R] : IsLocalRingHom (RingHom.id R)

Equations

• ⋯ = ⋯

@[simp]

theorem isUnit_map_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) : IsUnit (f a) ↔ IsUnit a

@[simp]

theorem map_mem_nonunits_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) : f a ∈ nonunits S ↔ a ∈ nonunits R

instance isLocalRingHom_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (g : S →+* T) (f : R →+* S) [IsLocalRingHom g] [IsLocalRingHom f] : IsLocalRingHom (g.comp f)

Equations

• ⋯ = ⋯

instance isLocalRingHom_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R ≃+* S) : IsLocalRingHom ↑f

Equations

• ⋯ = ⋯

@[simp]

theorem isUnit_of_map_unit {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) (h : IsUnit (f a)) : IsUnit a

theorem of_irreducible_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : IsLocalRingHom f] {x : R} (hfx : Irreducible (f x)) : Irreducible x

theorem isLocalRingHom_of_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) [IsLocalRingHom (g.comp f)] : IsLocalRingHom f

theorem RingHom.domain_localRing {R : Type u_1} {S : Type u_2} [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.

theorem map_nonunit {R : Type u} {S : Type v} [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.

theorem LocalRing.local_hom_TFAE {R : Type u} {S : Type v} [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

theorem LocalRing.of_surjective {R : Type u} {S : Type v} [CommSemiring R] [LocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S) [IsLocalRingHom f] (hf : Function.Surjective ⇑f) : LocalRing S

theorem LocalRing.surjective_units_map_of_local_ringHom {R : Type u} {S : Type v} [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.

def LocalRing.ResidueField (R : Type u) [CommRing R] [LocalRing R] : Type u

The residue field of a local ring is the quotient of the ring by its maximal ideal.

Equations

• LocalRing.ResidueField R = (R ⧸ LocalRing.maximalIdeal R)

instance LocalRing.ResidueFieldCommRing (R : Type u) [CommRing R] [LocalRing R] : CommRing (LocalRing.ResidueField R)

Equations

• LocalRing.ResidueFieldCommRing R = let_fun this := inferInstance; this

instance LocalRing.ResidueFieldInhabited (R : Type u) [CommRing R] [LocalRing R] : Inhabited (LocalRing.ResidueField R)

Equations

• LocalRing.ResidueFieldInhabited R = let_fun this := inferInstance; this

noncomputable instance LocalRing.ResidueField.field (R : Type u) [CommRing R] [LocalRing R] : Field (LocalRing.ResidueField R)

Equations

• LocalRing.ResidueField.field R = Ideal.Quotient.field (LocalRing.maximalIdeal R)

def LocalRing.residue (R : Type u) [CommRing R] [LocalRing R] : R →+* LocalRing.ResidueField R

The quotient map from a local ring to its residue field.

Equations

• LocalRing.residue R = Ideal.Quotient.mk (LocalRing.maximalIdeal R)

instance LocalRing.ResidueField.algebra (R : Type u) [CommRing R] [LocalRing R] : Algebra R (LocalRing.ResidueField R)

Equations

• LocalRing.ResidueField.algebra R = Ideal.Quotient.algebra R

theorem LocalRing.ResidueField.algebraMap_eq (R : Type u) [CommRing R] [LocalRing R] : algebraMap R (LocalRing.ResidueField R) = LocalRing.residue R

instance LocalRing.instIsLocalRingHomResidueFieldResidue (R : Type u) [CommRing R] [LocalRing R] : IsLocalRingHom (LocalRing.residue R)

Equations

• ⋯ = ⋯

def LocalRing.ResidueField.lift {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalRingHom f] : LocalRing.ResidueField R →+* S

A local ring homomorphism into a field can be descended onto the residue field.

Equations

• LocalRing.ResidueField.lift f = Ideal.Quotient.lift (LocalRing.maximalIdeal R) f ⋯

theorem LocalRing.ResidueField.lift_comp_residue {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalRingHom f] : (LocalRing.ResidueField.lift f).comp (LocalRing.residue R) = f

@[simp]

theorem LocalRing.ResidueField.lift_residue_apply {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalRingHom f] (x : R) : (LocalRing.ResidueField.lift f) ((LocalRing.residue R) x) = f x

def LocalRing.ResidueField.map {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] : LocalRing.ResidueField R →+* LocalRing.ResidueField S

The map on residue fields induced by a local homomorphism between local rings

Equations

• LocalRing.ResidueField.map f = Ideal.Quotient.lift (LocalRing.maximalIdeal R) ((Ideal.Quotient.mk (LocalRing.maximalIdeal S)).comp f) ⋯

@[simp]

theorem LocalRing.ResidueField.map_id {R : Type u} [CommRing R] [LocalRing R] : LocalRing.ResidueField.map (RingHom.id R) = RingHom.id (LocalRing.ResidueField R)

Applying LocalRing.ResidueField.map to the identity ring homomorphism gives the identity ring homomorphism.

theorem LocalRing.ResidueField.map_comp {R : Type u} {S : Type v} {T : Type w} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (f : T →+* R) (g : R →+* S) [IsLocalRingHom f] [IsLocalRingHom g] : LocalRing.ResidueField.map (g.comp f) = (LocalRing.ResidueField.map g).comp (LocalRing.ResidueField.map f)

The composite of two LocalRing.ResidueField.maps is the LocalRing.ResidueField.map of the composite.

theorem LocalRing.ResidueField.map_comp_residue {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] : (LocalRing.ResidueField.map f).comp (LocalRing.residue R) = (LocalRing.residue S).comp f

theorem LocalRing.ResidueField.map_residue {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] (r : R) : (LocalRing.ResidueField.map f) ((LocalRing.residue R) r) = (LocalRing.residue S) (f r)

theorem LocalRing.ResidueField.map_id_apply {R : Type u} [CommRing R] [LocalRing R] (x : LocalRing.ResidueField R) : (LocalRing.ResidueField.map (RingHom.id R)) x = x

@[simp]

theorem LocalRing.ResidueField.map_map {R : Type u} {S : Type v} {T : Type w} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (f : R →+* S) (g : S →+* T) (x : LocalRing.ResidueField R) [IsLocalRingHom f] [IsLocalRingHom g] : (LocalRing.ResidueField.map g) ((LocalRing.ResidueField.map f) x) = (LocalRing.ResidueField.map (g.comp f)) x

@[simp]

theorem LocalRing.ResidueField.mapEquiv_apply {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) (a : LocalRing.ResidueField R) : (LocalRing.ResidueField.mapEquiv f) a = (LocalRing.ResidueField.map ↑f) a

def LocalRing.ResidueField.mapEquiv {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) : LocalRing.ResidueField R ≃+* LocalRing.ResidueField S

A ring isomorphism defines an isomorphism of residue fields.

Equations

• LocalRing.ResidueField.mapEquiv f = { toFun := ⇑(LocalRing.ResidueField.map ↑f), invFun := ⇑(LocalRing.ResidueField.map ↑f.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem LocalRing.ResidueField.mapEquiv.symm {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) : (LocalRing.ResidueField.mapEquiv f).symm = LocalRing.ResidueField.mapEquiv f.symm

@[simp]

theorem LocalRing.ResidueField.mapEquiv_trans {R : Type u} {S : Type v} {T : Type w} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T) : LocalRing.ResidueField.mapEquiv (e₁.trans e₂) = (LocalRing.ResidueField.mapEquiv e₁).trans (LocalRing.ResidueField.mapEquiv e₂)

@[simp]

theorem LocalRing.ResidueField.mapEquiv_refl {R : Type u} [CommRing R] [LocalRing R] : LocalRing.ResidueField.mapEquiv (RingEquiv.refl R) = RingEquiv.refl (LocalRing.ResidueField R)

@[simp]

theorem LocalRing.ResidueField.mapAut_apply {R : Type u} [CommRing R] [LocalRing R] (f : R ≃+* R) : LocalRing.ResidueField.mapAut f = LocalRing.ResidueField.mapEquiv f

def LocalRing.ResidueField.mapAut {R : Type u} [CommRing R] [LocalRing R] : RingAut R →* RingAut (LocalRing.ResidueField R)

The group homomorphism from RingAut R to RingAut k where k is the residue field of R.

Equations

• LocalRing.ResidueField.mapAut = { toFun := LocalRing.ResidueField.mapEquiv, map_one' := ⋯, map_mul' := ⋯ }

instance LocalRing.ResidueField.instMulSemiringAction {R : Type u} [CommRing R] [LocalRing R] (G : Type u_1) [Group G] [MulSemiringAction G R] : MulSemiringAction G (LocalRing.ResidueField R)

If G acts on R as a MulSemiringAction, then it also acts on LocalRing.ResidueField R.

Equations

• LocalRing.ResidueField.instMulSemiringAction G = MulSemiringAction.compHom (LocalRing.ResidueField R) (LocalRing.ResidueField.mapAut.comp (MulSemiringAction.toRingAut G R))

@[simp]

theorem LocalRing.ResidueField.residue_smul {R : Type u} [CommRing R] [LocalRing R] (G : Type u_1) [Group G] [MulSemiringAction G R] (g : G) (r : R) : (LocalRing.residue R) (g • r) = g • (LocalRing.residue R) r

theorem LocalRing.ker_eq_maximalIdeal {R : Type u} {K : Type u'} [CommRing R] [LocalRing R] [Field K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) : RingHom.ker φ = LocalRing.maximalIdeal R

theorem LocalRing.isLocalRingHom_residue {R : Type u} [CommRing R] [LocalRing R] : IsLocalRingHom (LocalRing.residue R)

@[instance 100]

instance Field.instLocalRing (K : Type u') [Field K] : LocalRing K

Equations

• ⋯ = ⋯

theorem LocalRing.maximalIdeal_eq_bot {R : Type u_1} [Field R] : LocalRing.maximalIdeal R = ⊥

theorem RingEquiv.localRing {A : Type u_1} {B : Type u_2} [CommSemiring A] [LocalRing A] [CommSemiring B] (e : A ≃+* B) : LocalRing B