Serre's mass formulas

Let K be a nonarchimedean local field whose residue field has q elements, and let σ_K(n) be the set of totally ramified subextensions of degree n of a separable closure of K. For L ∈ σ_K(n) with discriminant exponent d(L), the wild exponent is c(L) = d(L) - n + 1. Serre's first mass formula states that ∑_{L ∈ σ_K(n)} q ^ (-c(L)) = n. The sum is taken in ℝ≥0∞, so the equation also asserts that it is finite. For n = 0 both sides vanish, since σ_K(0) is empty.

The proof integrates root counts over the Eisenstein region of coefficient space against Haar measure normalized on the integer box. Almost every Eisenstein polynomial is separable and irreducible of degree n, and each of its roots generates exactly one member of σ_K(n), so its numbers of roots in the members of σ_K(n) add up to n. Hence the root-count integrals add up to n times the volume of the region. The root count of L integrates to q ^ (-(d(L) + 1)) (1 - q⁻¹), which is q ^ (-c(L)) times that volume.

The remaining statements of Serre's note follow from the first formula and the reductions already proved for the weighted count:

• for 0 < n, regrouping along isomorphism classes gives the second mass formula ∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = 1 for every set of representatives R;
• for 0 < n, σ_K(n) is infinite exactly when K has equal characteristic p and p ∣ n;
• the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) converges to n, also when σ_K(n) is infinite;
• if the residue characteristic does not divide n, then σ_K(n) has exactly n elements.

Main results

• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent: the first mass formula.
• IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent: the second mass formula.
• TauCeti.infinite_totallyRamifiedOfDegree_iff: the finiteness dichotomy.
• TauCeti.hasSum_one_div_natCard_residueField_pow_wildExponent and TauCeti.summable_one_div_natCard_residueField_pow_wildExponent: convergence of the real series.
• TauCeti.encard_totallyRamifiedOfDegree_of_not_dvd: the tame count.

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, Théorèmes 1 and 2, Remarques 1° and 3°.

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

Serre's first mass formula: the totally ramified degree-n subextensions L of a separable closure of K satisfy ∑_L q ^ (-c(L)) = n, where q is the residue cardinality of K and c(L) is the wild exponent.

theorem TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} (hR : IsRepresentativeSet n R) (hn : 0 < n) : ∑' (M : ↑R), 1 / (↑(Nat.card Gal(↥↑M/K)) * ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑M).wildExponent) = 1

Serre's second mass formula: for 0 < n and every set R of representatives of the K-isomorphism classes in σ_K(n), ∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = 1.

theorem TauCeti.infinite_totallyRamifiedOfDegree_iff {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

Serre's finiteness dichotomy: for 0 < n, there are infinitely many totally ramified degree-n subextensions of a separable closure of K exactly when K has equal characteristic p, the residue characteristic, and p ∣ n.

theorem TauCeti.hasSum_one_div_natCard_residueField_pow_wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} : HasSum (fun (L : ↑(totallyRamifiedOfDegree K n)) => 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent) ↑n

The real form of the first mass formula: the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) converges to n, also when σ_K(n) is infinite.

theorem TauCeti.summable_one_div_natCard_residueField_pow_wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} : Summable fun (L : ↑(totallyRamifiedOfDegree K n)) => 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent

Convergence of the weighted count: the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) converges, also when σ_K(n) is infinite.

theorem TauCeti.encard_totallyRamifiedOfDegree_of_not_dvd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hp : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) : (totallyRamifiedOfDegree K n).encard = ↑n

The tame count: if the residue characteristic of K does not divide n, then a separable closure of K has exactly n totally ramified subextensions of degree n.