Residue Field of local rings

Main definitions

• LocalRing.ResidueField: The quotient of a local ring by its maximal ideal.
• LocalRing.residue: The quotient map from a local ring to its residue field.

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

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_1) [CommRing R] [LocalRing R] : CommRing (LocalRing.ResidueField R)

Equations

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

instance LocalRing.ResidueFieldInhabited (R : Type u_1) [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_1) [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_1) [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)