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} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime] (f : R →+* S) (hf : I = comap f J) : I.ResidueField →+* J.ResidueField

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

Equations

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

@[simp]

theorem Ideal.ResidueField.map_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime] (f : R →+* S) (hf : I = comap f J) (r : R) : (map I J f hf) ((algebraMap R I.ResidueField) r) = (algebraMap S J.ResidueField) (f r)

theorem RingHom.SurjectiveOnStalks.residueFieldMap_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (H : f.SurjectiveOnStalks) (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime] (hf : I = Ideal.comap f J) : Function.Bijective ⇑(Ideal.ResidueField.map I J f hf)

noncomputable def Ideal.ResidueField.mapₐ {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsPrime] (J : Ideal B) [J.IsPrime] (f : A →ₐ[R] B) (hf : I = comap f.toRingHom J) : I.ResidueField →ₐ[R] J.ResidueField

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

Equations

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

@[simp]

theorem Ideal.ResidueField.mapₐ_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsPrime] (J : Ideal B) [J.IsPrime] (f : A →ₐ[R] B) (hf : I = comap f.toRingHom J) (x : I.ResidueField) : (mapₐ I J f hf) x = (map I J f.toRingHom 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

@[implicit_reducible]

noncomputable 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} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal A) [I.IsPrime] : IsScalarTower R (A ⧸ I) I.ResidueField

instance instLiesOverResidueFieldBotIdeal {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : ⊥.LiesOver I

@[simp]

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

@[deprecated Ideal.algebraMap_quotient_residueField_mk (since := "2025-12-02")]

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

Alias of Ideal.algebraMap_quotient_residueField_mk.

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

instance instIsFractionRingResidueFieldBotIdeal {R : Type u_1} [CommRing R] [IsDomain R] : IsFractionRing R ⊥.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)

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

instance instFiniteResidueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsMaximal] : Module.Finite R I.ResidueField

noncomputable def Ideal.algEquivResidueFieldOfField {k : Type u_5} [Field k] (p : Ideal k) [p.IsPrime] : k ≃ₐ[k] p.ResidueField

The equivalence between a field and the residue field of its prime ideal, induced by the algebra map.

Equations

• p.algEquivResidueFieldOfField = AlgEquiv.ofBijective (Algebra.ofId k p.ResidueField) ⋯

@[simp]

theorem Ideal.algEquivResidueFieldOfField_apply {k : Type u_5} [Field k] (p : Ideal k) [p.IsPrime] (x : k) : p.algEquivResidueFieldOfField x = (algebraMap k p.ResidueField) x

theorem Ideal.surjectiveOnStalks_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] : (algebraMap R I.ResidueField).SurjectiveOnStalks

instance instIsLocalHomAtPrimeRingHomAlgebraMap {R : Type u_1} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [Localization.AtPrime.IsLiesOverAlgebra I J] : IsLocalHom (algebraMap (Localization.AtPrime I) (Localization.AtPrime J))

noncomputable def Ideal.residueFieldRingEquiv {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (J : Ideal A) (K : Ideal B) [J.IsPrime] [K.IsPrime] (f : A ≃+* B) (h : J = comap f K) : J.ResidueField ≃+* K.ResidueField

An isomorphism of rings induces an isomorphism of residue fields.

Equations

• J.residueFieldRingEquiv K f h = IsLocalRing.ResidueField.mapEquiv (Localization.localRingEquiv J K f h)

@[reducible, inline]

noncomputable abbrev Ideal.residueFieldAlgEquiv {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (J : Ideal A) (K : Ideal B) [J.IsPrime] [K.IsPrime] (f : A ≃ₐ[R] B) (h : J = comap f K) : J.ResidueField ≃ₐ[R] K.ResidueField

An isomorphism of rings induces an isomorphism of residue fields.

Equations

• J.residueFieldAlgEquiv K f h = IsLocalRing.ResidueField.mapAlgEquiv (Localization.localAlgEquiv J K f h)

@[reducible, inline]

noncomputable abbrev Ideal.residueFieldAlgEquiv' {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal R) [I.IsPrime] (J : Ideal A) (K : Ideal B) [J.IsPrime] [K.IsPrime] [J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [Localization.AtPrime.IsLiesOverAlgebra I J] [K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [Localization.AtPrime.IsLiesOverAlgebra I K] (f : A ≃ₐ[R] B) (h : J = comap f K) : J.ResidueField ≃ₐ[I.ResidueField] K.ResidueField

An isomorphism of rings induces an isomorphism of residue fields.

Equations

• I.residueFieldAlgEquiv' J K f h = IsLocalRing.ResidueField.mapAlgEquiv' (Localization.localAlgEquiv' I J K f h)

instance instEssFiniteTypeResidueField {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] : Algebra.EssFiniteType R p.ResidueField

instance instEssFiniteTypeResidueField_1 {R : Type u_1} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [Algebra.EssFiniteType R A] (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q] : Algebra.EssFiniteType p.ResidueField q.ResidueField

noncomputable def Ideal.ResidueField.lift {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [I.IsPrime] (f : R →+* S) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)) : I.ResidueField →+* S

If f sends I to 0 and Iᶜ to units, then f lifts to κ(I).

Equations

• Ideal.ResidueField.lift I f hf₁ hf₂ = IsLocalization.lift ⋯

@[simp]

theorem Ideal.ResidueField.lift_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [I.IsPrime] (f : R →+* S) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)) (r : R) : (lift I f hf₁ hf₂) ((algebraMap R I.ResidueField) r) = f r

noncomputable def Ideal.ResidueField.liftₐ {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)) : I.ResidueField →ₐ[R] B

If f sends I to 0 and Iᶜ to units, then f lifts to κ(I).

Equations

• Ideal.ResidueField.liftₐ I f hf₁ hf₂ = { toRingHom := Ideal.ResidueField.lift I f.toRingHom hf₁ hf₂, commutes' := ⋯ }

@[simp]

theorem Ideal.ResidueField.liftₐ_algebraMap {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)) (r : A) : (liftₐ I f hf₁ hf₂) ((algebraMap A I.ResidueField) r) = f r

@[simp]

theorem Ideal.ResidueField.liftₐ_comp_toAlgHom {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)) : (liftₐ I f hf₁ hf₂).comp (IsScalarTower.toAlgHom R A I.ResidueField) = f

theorem Ideal.ResidueField.ringHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal R} [I.IsPrime] {f g : I.ResidueField →+* S} (H : f.comp (algebraMap R I.ResidueField) = g.comp (algebraMap R I.ResidueField)) : f = g

theorem Ideal.ResidueField.ringHom_ext_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal R} [I.IsPrime] {f g : I.ResidueField →+* S} : f = g ↔ f.comp (algebraMap R I.ResidueField) = g.comp (algebraMap R I.ResidueField)

theorem Ideal.ResidueField.algHom_ext {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {I : Ideal A} [I.IsPrime] {f g : I.ResidueField →ₐ[R] B} (H : f.comp (IsScalarTower.toAlgHom R A I.ResidueField) = g.comp (IsScalarTower.toAlgHom R A I.ResidueField)) : f = g

theorem Ideal.ResidueField.algHom_ext_iff {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {I : Ideal A} [I.IsPrime] {f g : I.ResidueField →ₐ[R] B} : f = g ↔ f.comp (IsScalarTower.toAlgHom R A I.ResidueField) = g.comp (IsScalarTower.toAlgHom R A I.ResidueField)