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.

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

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

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

@[instance_reducible]

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

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

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

instance instFiniteResidueFieldOfQuotientIdeal {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] [Finite (R ⧸ I)] : Finite 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)

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.

@[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)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime 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.

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

@[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)] [K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)] [IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime 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.

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)] [IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime 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).

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

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

@[simp]

theorem Ideal.ResidueField.mapₐ_id {R : Type u_1} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal A) [I.IsPrime] : mapₐ I I (AlgHom.id R A) ⋯ = AlgHom.id R I.ResidueField