Finiteness of the totally ramified extensions of given degree

Let K be a nonarchimedean local field with residue field of cardinality q, and let 0 < n. Serre's mass formula ∑_{L ∈ σ_K(n)} q ^ (-c(L)) = n decides whether the family σ_K(n) = totallyRamifiedOfDegree K n is finite. Outside the case where K has characteristic p > 0 and p ∣ n, that is when (n : K) ≠ 0, the wild exponents of the members of σ_K(n) are bounded: by the upper bound of Dedekind's different theorem, d(L) ≤ n - 1 + v_L(n), and v_L(n) = n · v_K(n) since L / K is totally ramified of degree n, so c(L) ≤ n · v_K(n). Every weight q ^ (-c(L)) is then at least q ^ (-n · v_K(n)), and the weighted sum is finite exactly when σ_K(n) is finite. In the tame case, when the residue characteristic does not divide n, every weight is 1 and the weighted sum is the cardinality of σ_K(n).

Together with the converse half, that σ_K(n) is infinite when (n : K) = 0 (TauCeti.infinite_totallyRamifiedOfDegree), this says that σ_K(n) is infinite exactly when K has equal characteristic p with p ∣ n or the weighted sum is infinite. The mass formula, which makes the weighted sum n, then gives Serre's finiteness dichotomy; it also gives the tame count #σ_K(n) = n.

Main results

• IntermediateField.discriminantExponent_le_sub_one_add_mul_natCastValuation: for L ∈ σ_K(n) and (n : K) ≠ 0, d(L) ≤ n - 1 + n · v_K(n).
• IntermediateField.wildExponent_le_mul_natCastValuation: for L ∈ σ_K(n) and (n : K) ≠ 0, c(L) ≤ n · v_K(n).
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_ne_top_iff_finite: for (n : K) ≠ 0, ∑_{L ∈ σ_K(n)} q ^ (-c(L)) is finite exactly when σ_K(n) is finite.
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_encard: if the residue characteristic does not divide n, ∑_{L ∈ σ_K(n)} q ^ (-c(L)) is the cardinality of σ_K(n).
• TauCeti.infinite_totallyRamifiedOfDegree_iff_or_tsum_eq_top: for 0 < n, σ_K(n) is infinite exactly when K has equal characteristic p with p ∣ n, or ∑_{L ∈ σ_K(n)} q ^ (-c(L)) is infinite.

References

• J.-P. Serre, Une « formule de masse » pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris Sér. A 286 (1978), 1031–1036, Remarque 1°.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.

theorem IntermediateField.discriminantExponent_le_sub_one_add_mul_natCastValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) (hnK : ↑n ≠ 0) : L.discriminantExponent ≤ n - 1 + n * TauCeti.natCastValuation K n hnK

The discriminant bound for σ_K(n) away from equal characteristic p ∣ n: if n is nonzero in K, the discriminant exponent of L ∈ σ_K(n) is at most n - 1 + n · v_K(n). Since L / K is totally ramified, d(L) is the different exponent, so this is differentExponent_le_ramificationIndex_sub_one_add_natCastValuation with e(L / K) = n, together with v_L(n) = n · v_K(n).

theorem IntermediateField.wildExponent_le_mul_natCastValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) (hnK : ↑n ≠ 0) : L.wildExponent ≤ n * TauCeti.natCastValuation K n hnK

The wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n: if n is nonzero in K, every L ∈ σ_K(n) has c(L) ≤ n · v_K(n). In equal characteristic, where v_K(n) = 0, this recovers c(L) = 0 for p ∤ n.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_ne_top_iff_finite {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hnK : ↑n ≠ 0) : ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent ≠ ⊤ ↔ (totallyRamifiedOfDegree K n).Finite

Finiteness of σ_K(n) away from equal characteristic p ∣ n: if n is nonzero in K, the weighted count ∑_{L ∈ σ_K(n)} q ^ (-c(L)) of Serre's mass formula is finite exactly when σ_K(n) is finite. With the mass formula, this makes σ_K(n) finite.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_encard {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) : ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ↑(totallyRamifiedOfDegree K n).encard

The tame count, weighted form: if the residue characteristic of K does not divide n, every member of σ_K(n) has weight q ^ (-c(L)) = 1, so the weighted count ∑_{L ∈ σ_K(n)} q ^ (-c(L)) of Serre's mass formula is the cardinality of σ_K(n). With the mass formula, σ_K(n) has exactly n elements.

theorem TauCeti.infinite_totallyRamifiedOfDegree_iff_or_tsum_eq_top {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) : (totallyRamifiedOfDegree K n).Infinite ↔ ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∧ ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n ∨ ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ⊤

Serre's finiteness dichotomy, relative to the weighted count: for 0 < n, σ_K(n) is infinite exactly when K has equal characteristic p, the residue characteristic, with p ∣ n, or the weighted count ∑_{L ∈ σ_K(n)} q ^ (-c(L)) of Serre's mass formula is infinite. Since the mass formula makes that count n, the second alternative never occurs.