The residue degree of a completion is the inertia degree

Let R ⊆ B be Dedekind domains with fraction fields K ⊆ L, and let w be a height-one prime of B lying over the height-one prime v of R. The completions K_v and L_w carry valuative relations, and the canonical map K_v → L_w is a valuative extension, so the residue field 𝓀[L_w] is an extension of the residue field 𝓀[K_v]. Its degree is the residue degree of the local extension.

This file proves that this local residue degree is the global inertia degree f(w ∣ v): the residue-field identifications R ⧸ v ≃+* 𝓀[K_v] and B ⧸ w ≃+* 𝓀[L_w] intertwine the two residue extensions, so the two degrees agree. Together with IsDedekindDomain.HeightOneSpectrum.ramificationIndex_adicCompletion, which matches the local ramification index with w.asIdeal.ramificationIdx R, this says that passing to the completions loses neither of the two invariants attached to w over v.

Main results

• IsDedekindDomain.HeightOneSpectrum.algebraMap_residueFieldEquivAdicCompletion: the residue-field identifications intertwine the residue extension of w over v with the residue extension of the completions.
• IsDedekindDomain.HeightOneSpectrum.finrank_residueField_adicCompletion: the residue degree of L_w / K_v is w.asIdeal.inertiaDeg R.
• IsDedekindDomain.HeightOneSpectrum.natCard_residueField_adicCompletion_eq_pow_inertiaDeg: for finite residue fields, #𝓀[L_w] = #𝓀[K_v] ^ f(w ∣ v).

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §6 and §8.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_residueFieldEquivAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : R ⧸ v.asIdeal) : (algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion L w)).integer)) (v.residueFieldEquivAdicCompletion x) = w.residueFieldEquivAdicCompletion ((algebraMap (R ⧸ v.asIdeal) (B ⧸ w.asIdeal)) x)

The residue-field identifications are natural. The identifications R ⧸ v ≃+* 𝓀[K_v] and B ⧸ w ≃+* 𝓀[L_w] intertwine the residue extension of w over v with the residue extension of the completions.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.finrank_residueField_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : Module.finrank (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion L w)).integer) = w.asIdeal.inertiaDeg R

The local residue degree is the global inertia degree. For w a height-one prime of B over the height-one prime v of R, the residue field of the completion L_w has degree w.asIdeal.inertiaDeg R over the residue field of K_v.

theorem IsDedekindDomain.HeightOneSpectrum.natCard_residueField_adicCompletion_eq_pow_inertiaDeg {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] [Finite (B ⧸ w.asIdeal)] : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion L w)).integer) = Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer) ^ w.asIdeal.inertiaDeg R

The residue cardinality of a completion. When the residue field of w is finite, the residue field of L_w has #𝓀[K_v] ^ f(w ∣ v) elements.