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.

source

@[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)

Instances For

source

@[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)

Instances For

source

@[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)

source

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' := ⋯ }

Instances For

source

@[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

source

@[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

source

@[simp]

theorem Ideal.ker_algebraMap_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] :

RingHom.ker (algebraMap R I.ResidueField) = I

source

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

source

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

IsScalarTower R (R ⧸ I) I.ResidueField

source

@[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

source

@[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.

source

theorem Ideal.injective_algebraMap_quotient_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] :

Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)

source

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

IsFractionRing (R ⧸ I) I.ResidueField

source

theorem Ideal.bijective_algebraMap_quotient_residueField {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsMaximal] :

Function.Bijective ⇑(algebraMap (R ⧸ I) I.ResidueField)

source

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

(algebraMap R I.ResidueField).SurjectiveOnStalks

source

instance instIsLocalHomAtPrimeRingHomAlgebraMap {R : Type u_1} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] :

IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))

source

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 ⋯

Instances For

source

@[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

source

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' := ⋯ }

Instances For

source

@[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

source

@[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

source

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

source

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)

source

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

source

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)

Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

The residue field of a prime ideal #