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)

Instances For

• LocalRing.ResidueField.algebra
• LocalRing.ResidueField.field
• LocalRing.ResidueField.finiteDimensional_of_noetherian
• LocalRing.ResidueField.instAlgebra
• LocalRing.ResidueField.instAlgebra_1
• LocalRing.ResidueField.instIsScalarTower
• LocalRing.ResidueField.instMulSemiringAction
• LocalRing.ResidueFieldCommRing
• LocalRing.ResidueFieldInhabited

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

Equations

• LocalRing.ResidueFieldCommRing R = inferInstance

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

Equations

• LocalRing.ResidueFieldInhabited R = inferInstance

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)

Instances For

• LocalRing.instIsLocalRingHomResidueFieldResidue