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.instCommRingResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] : CommRing (ResidueField R)

Equations

• IsLocalRing.instCommRingResidueField R = Ideal.Quotient.commRing (IsLocalRing.maximalIdeal R)

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

Equations

• IsLocalRing.instInhabitedResidueField R = Submodule.Quotient.instInhabitedQuotient (IsLocalRing.maximalIdeal R)

noncomputable instance IsLocalRing.ResidueField.field (R : Type u_1) [CommRing R] [IsLocalRing R] : Field (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 →+* ResidueField R

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

Equations

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