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)

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• IsLocalRing.instInhabitedResidueField R = { default := IsLocalRing.instInhabitedResidueField._aux_1 R }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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)