The residue field of a prime ideal

We define Ideal.ResidueField I to be the residue field of the local ring Localization.Prime I, and provide an IsFractionRing (R ⧸ I) I.ResidueField instance.

@[reducible, inline]

abbrev Ideal.ResidueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Type u_1

The residue field at a prime ideal, defined to be the residue field of the local ring Localization.Prime I. We also provide an IsFractionRing (R ⧸ I) I.ResidueField instance.

Equations

• I.ResidueField = IsLocalRing.ResidueField (Localization.AtPrime I)

@[reducible, inline]

noncomputable abbrev Ideal.ResidueField.map {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (f : R →+* A) (hf : I = Ideal.comap f J) : I.ResidueField →+* J.ResidueField

If I = f⁻¹(J), then there is an canonical embedding κ(I) ↪ κ(J).

Equations

• Ideal.ResidueField.map I J f hf = IsLocalRing.ResidueField.map (Localization.localRingHom I J f hf)

noncomputable def Ideal.ResidueField.mapₐ {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (hf : I = Ideal.comap (algebraMap R A) J) : I.ResidueField →ₐ[R] J.ResidueField

If I = f⁻¹(J), then there is an canonical embedding κ(I) ↪ κ(J).

Equations

• Ideal.ResidueField.mapₐ I J hf = { toRingHom := Ideal.ResidueField.map I J (algebraMap R A) hf, commutes' := ⋯ }

@[simp]

theorem Ideal.ResidueField.mapₐ_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (hf : I = Ideal.comap (algebraMap R A) J) (x : I.ResidueField) : (Ideal.ResidueField.mapₐ I J hf) x = (Ideal.ResidueField.map I J (algebraMap R A) hf) x

@[simp]

theorem Ideal.algebraMap_residueField_eq_zero {R : Type u_1} [CommRing R] {I : Ideal R} [I.IsPrime] {x : R} : (algebraMap R I.ResidueField) x = 0 ↔ x ∈ I

@[simp]

theorem Ideal.ker_algebraMap_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : RingHom.ker (algebraMap R I.ResidueField) = I

instance instAlgebraQuotientIdealResidueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Algebra (R ⧸ I) I.ResidueField

Equations

• instAlgebraQuotientIdealResidueField I = (Ideal.Quotient.liftₐ I (Algebra.ofId R I.ResidueField) ⋯).toAlgebra

instance instIsScalarTowerQuotientIdealResidueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : IsScalarTower R (R ⧸ I) I.ResidueField

@[simp]

theorem algebraMap_mk {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (x : R) : (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x) = (algebraMap R I.ResidueField) x

theorem Ideal.injective_algebraMap_quotient_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)

instance instIsFractionRingQuotientIdealResidueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : IsFractionRing (R ⧸ I) I.ResidueField

theorem Ideal.bijective_algebraMap_quotient_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsMaximal] : Function.Bijective ⇑(algebraMap (R ⧸ I) I.ResidueField)