Hilbert's formula for the different exponent

Let L/K be a finite Galois extension of nonarchimedean local fields with group G, and let G_i be its lower ramification groups. Hilbert's formula computes the different exponent d(L/K) from the ramification filtration:

d(L/K) = ∑_{i ≥ 0} (#G_i - 1).

The proof is Serre's. The ring of integers 𝒪[L] is generated over 𝒪[K] by a single element x, so the different is generated by f'(x) for the minimal polynomial f of x, and f'(x) = ∏_{σ ≠ 1} (x - σ x) because the conjugates of x are its images under the Galois group. Hence d(L/K) = ∑_{σ ≠ 1} v_L(σ x - x), and σ lies in G_i exactly when v_L(σ x - x) ≥ i + 1, so each σ ≠ 1 contributes 1 to exactly v_L(σ x - x) of the terms #G_i - 1.

Main results

• TauCeti.natCast_differentExponent_eq_sum_addVal_smul_sub: d(L/K) = ∑_{σ ≠ 1} v_L(σ x - x) for a generator x of 𝒪[L] over 𝒪[K].
• TauCeti.differentExponent_eq_finsum_lowerRamificationGroup: Hilbert's formula.
• TauCeti.sum_range_card_lowerRamificationGroup_sub_one_le_differentExponent: its truncations bound the different exponent from below.
• TauCeti.differentExponent_eq_of_lowerRamificationGroup_eq_at_zero_eq_bot: the single-break specialization of Hilbert's formula, d(L/K) = (t + 1)(#G₀ - 1).

References

• J.-P. Serre, Corps Locaux, Chapter IV, §1, Proposition 4.
• J. Neukirch, Algebraic Number Theory, Chapter II, §10.

theorem TauCeti.natCast_differentExponent_eq_sum_addVal_smul_sub (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] [Module.Finite K L] [IsGalois K L] [DecidableEq Gal(L/K)] {x : ↥(ValuativeRel.valuation L).integer} (hx : (↥(ValuativeRel.valuation K).integer)[x] = ⊤) : ↑(differentExponent K L) = ∑ σ ∈ Finset.univ.erase 1, (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (σ • x - x)

The different exponent at a generator. If x generates 𝒪[L] over 𝒪[K], then d(L/K) = ∑_{σ ≠ 1} v_L(σ x - x), the sum running over the nontrivial automorphisms of L/K.

theorem TauCeti.differentExponent_eq_finsum_lowerRamificationGroup (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] [Module.Finite K L] [IsGalois K L] : differentExponent K L = ∑ᶠ (i : ℕ), (Nat.card ↥(LocalFieldsRamification.lowerRamificationGroup K L ↑i) - 1)

Hilbert's formula for the different exponent: for a finite Galois extension L/K of nonarchimedean local fields, d(L/K) = ∑_{i ≥ 0} (#G_i - 1), where G_i is the i-th lower ramification group. The sum is finite because the filtration is eventually trivial.

theorem TauCeti.sum_range_card_lowerRamificationGroup_sub_one_le_differentExponent (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] [Module.Finite K L] [IsGalois K L] (m : ℕ) : ∑ i ∈ Finset.range m, (Nat.card ↥(LocalFieldsRamification.lowerRamificationGroup K L ↑i) - 1) ≤ differentExponent K L

Hilbert's formula, truncated: for a finite Galois extension L/K of nonarchimedean local fields, ∑_{i < m} (#G_i - 1) ≤ d(L/K) for every m.

theorem TauCeti.differentExponent_eq_of_lowerRamificationGroup_eq_at_zero_eq_bot (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] [Module.Finite K L] [IsGalois K L] {t : ℕ} (ht : LocalFieldsRamification.lowerRamificationGroup K L ↑t = LocalFieldsRamification.lowerRamificationGroup K L 0) (ht' : LocalFieldsRamification.lowerRamificationGroup K L ↑(t + 1) = ⊥) : differentExponent K L = (t + 1) * (Nat.card ↥(LocalFieldsRamification.lowerRamificationGroup K L 0) - 1)

If the lower ramification filtration is constant through depth t and trivial at depth t + 1, the different exponent is (t + 1)(#G₀ - 1).