The quotient by a maximal ideal of a local ring

A local ring R has exactly one maximal ideal, so the quotient R ⧸ 𝔪 by any maximal ideal 𝔪 is the residue field κ. This file records that identification as an R-linear equivalence, so that a statement about the simple modules R ⧸ 𝔪 of an arbitrary commutative ring can be specialised to the residue field of a local ring.

Main declarations

• TauCeti.quotientEquivResidueField: R ⧸ 𝔪 ≃ₗ[R] κ for a maximal ideal 𝔪, sending the class of r to residue R r.

noncomputable def TauCeti.quotientEquivResidueField {R : Type u_1} [CommRing R] [IsLocalRing R] {𝔪 : Ideal R} (h𝔪 : 𝔪.IsMaximal) : (R ⧸ 𝔪) ≃ₗ[R] IsLocalRing.ResidueField R

The quotient of a local ring by a maximal ideal is its residue field, as an R-linear equivalence sending the class of r to residue R r.

@[simp]

theorem TauCeti.quotientEquivResidueField_mk {R : Type u_1} [CommRing R] [IsLocalRing R] {𝔪 : Ideal R} (h𝔪 : 𝔪.IsMaximal) (r : R) : (quotientEquivResidueField h𝔪) ((Ideal.Quotient.mk 𝔪) r) = (IsLocalRing.residue R) r

quotientEquivResidueField sends the class of r to its residue.