The residue degree of an extension of local fields, and e · f = [L : K]

Let L/K be an extension of nonarchimedean local fields whose valuations are compatible, in the sense of ValuativeExtension K L. This file defines the residue degree

TauCeti.inertiaDegree K L : ℕ

as the degree of 𝓀[L] over 𝓀[K], the second of the two invariants attached to such an extension, and proves the fundamental identity e · f = [L : K] relating them to the degree.

The identity is Mathlib's Ideal.sum_ramification_inertia_eq_finrank for 𝒪[L] over 𝒪[K], read through three facts: 𝓂[L] is the only prime of 𝒪[L] above 𝓂[K], by IsLocalRing.primesOver_eq, so the sum has a single term; 𝒪[L] is a finite free 𝒪[K]-module of rank [L : K], by TauCeti.finrank_integerRing; and the two intrinsic invariants of L/K are the ideal-theoretic invariants of 𝓂[L] over 𝒪[K]. Those comparisons, ramificationIndex_eq_ramificationIdx and inertiaDegree_eq_inertiaDeg, are stated separately: they are what lets Dedekind-level results about 𝒪[K] ⊆ 𝒪[L] be used on the valuation-theoretic side, and conversely.

Main definitions

• TauCeti.inertiaDegree: the residue degree f(L/K) of an extension of nonarchimedean local fields.

Main results

• TauCeti.primesOver_maximalIdeal_eq_singleton: 𝓂[L] is the unique prime of 𝒪[L] above 𝓂[K].
• TauCeti.inertiaDegree_eq_inertiaDeg: the intrinsic residue degree agrees with Ideal.inertiaDeg of 𝓂[L] over 𝒪[K].
• TauCeti.ramificationIndex_mul_inertiaDegree: the fundamental identity e · f = [L : K].
• TauCeti.isTotallyRamified_iff_inertiaDegree_eq_one: total ramification is equivalent to residue degree one; TauCeti.IsTotallyRamified.inertiaDegree_eq_one is the forward direction.
• TauCeti.isTotallyRamified_iff_surjective_algebraMap_residueField: total ramification is equivalent to surjectivity of the residue-field map.
• TauCeti.inertiaDegree_tower: multiplicativity f(M/K) = f(L/K) · f(M/L) in a tower.
• TauCeti.natCard_residueField: #𝓀[L] = #𝓀[K] ^ f(L/K).

References

• J.-P. Serre, Corps Locaux, Chapter I, §4.
• J. Neukirch, Algebraic Number Theory, Chapter II, §6.

noncomputable def TauCeti.inertiaDegree (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ℕ

The residue degree f(L/K) of an extension of nonarchimedean local fields with compatible valuations: the degree of the residue field of L over the residue field of K.

Equations

• TauCeti.inertiaDegree K L = Module.finrank (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

theorem TauCeti.inertiaDegree_def (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : inertiaDegree K L = Module.finrank (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

The defining formula of inertiaDegree: the degree of the residue extension.

theorem TauCeti.inertiaDegree_pos {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : 0 < inertiaDegree K L

The residue degree is positive.

theorem TauCeti.natCard_residueField (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) = Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ inertiaDegree K L

The characteristic property of the residue degree: the residue field of L has #𝓀[K] ^ f(L/K) elements. The residue fields of nonarchimedean local fields are finite, so both cardinalities here are genuine.

theorem TauCeti.inertiaDegree_eq_inertiaDeg (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : inertiaDegree K L = (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer).inertiaDeg ↥(ValuativeRel.valuation K).integer

The residue degree is the ideal-theoretic inertia degree of 𝓂[L] over 𝒪[K].

theorem TauCeti.primesOver_maximalIdeal_eq_singleton (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer).primesOver ↥(ValuativeRel.valuation L).integer = {IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer}

The maximal ideal of 𝒪[L] is the unique prime above the maximal ideal of 𝒪[K].

theorem TauCeti.ramificationIndex_mul_inertiaDegree (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ramificationIndex K L * inertiaDegree K L = Module.finrank K L

The fundamental identity e(L/K) · f(L/K) = [L : K] for an extension of nonarchimedean local fields with compatible valuations.

theorem TauCeti.isTotallyRamified_iff_inertiaDegree_eq_one (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsTotallyRamified K L ↔ inertiaDegree K L = 1

A finite extension of nonarchimedean local fields is totally ramified if and only if its residue degree is one.

@[simp]

theorem TauCeti.IsTotallyRamified.inertiaDegree_eq_one {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) : inertiaDegree K L = 1

A totally ramified extension of nonarchimedean local fields has residue degree one.

theorem TauCeti.isTotallyRamified_iff_surjective_algebraMap_residueField (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsTotallyRamified K L ↔ Function.Surjective ⇑(algebraMap (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer))

A finite extension of nonarchimedean local fields is totally ramified if and only if every residue class of L comes from K.

theorem TauCeti.inertiaDegree_tower (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] [ValuativeExtension K M] : inertiaDegree K M = inertiaDegree K L * inertiaDegree L M

Multiplicativity of the residue degree in a tower M/L/K: f(M/K) = f(L/K) · f(M/L).

The compatibility of M over K is a hypothesis rather than a consequence of the two steps because f(M/K) is the degree of the residue extension 𝓀[M] / 𝓀[K], which that compatibility is what produces.