Residue Field of local rings

Main definitions

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

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

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

Equations

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

instance IsLocalRing.ResidueFieldCommRing (R : Type u_1) [CommRing R] [IsLocalRing R] : CommRing (IsLocalRing.ResidueField R)

Equations

• IsLocalRing.ResidueFieldCommRing R = inferInstance

instance IsLocalRing.ResidueFieldInhabited (R : Type u_1) [CommRing R] [IsLocalRing R] : Inhabited (IsLocalRing.ResidueField R)

Equations

• IsLocalRing.ResidueFieldInhabited R = inferInstance

noncomputable instance IsLocalRing.ResidueField.field (R : Type u_1) [CommRing R] [IsLocalRing R] : Field (IsLocalRing.ResidueField R)

Equations

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

def IsLocalRing.residue (R : Type u_1) [CommRing R] [IsLocalRing R] : R →+* IsLocalRing.ResidueField R

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

Equations

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

@[deprecated IsLocalRing.ResidueField (since := "2024-11-11")]

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

Alias of IsLocalRing.ResidueField.

---

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

Equations

• LocalRing.ResidueField = IsLocalRing.ResidueField

@[deprecated IsLocalRing.residue (since := "2024-11-11")]

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

Alias of IsLocalRing.residue.

---

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

Equations

• LocalRing.residue = IsLocalRing.residue