Root counts of Eisenstein polynomials in the counted extensions

For a subextension L and a coefficient vector a : Fin n → K, the root count L.rootCount a is the number of roots of the monic polynomial TauCeti.Polynomial.monicOfCoeff a lying in L, counted with multiplicity. Serre's proof of the mass formula integrates these root counts over the Eisenstein polynomials, and the identity that makes the integration work is that, at a separable Eisenstein polynomial of degree n, the root counts over all L ∈ σ_K(n) add up to n.

The reason is that an Eisenstein polynomial f of degree n is irreducible, so each of its roots x in the separable closure generates a member K⟮x⟯ of σ_K(n). Conversely a root x lies in a member L of σ_K(n) exactly when K⟮x⟯ = L, as both have degree n. The roots of f lying in L are therefore the roots generating L, and summing over L counts every root of f exactly once. The identification of the roots in L with its generators is IntermediateField.rootCount_eq_card_filter_adjoin_eq, which holds for any irreducible polynomial. When f is separable it has n roots in the separable closure. Separability is needed: an inseparable Eisenstein polynomial, which exists in equal characteristic, is irreducible and so has no root at all in the separable closure.

For additive Haar measure, the inseparable Eisenstein polynomials form a null set, so the sum identity holds almost everywhere on the Eisenstein region, including in equal characteristic.

For a single L ∈ σ_K(n), the root count of an Eisenstein polynomial is a finite sum of ball indicators: if the uniformizers of L are covered by pairwise disjoint balls of order r larger than the discriminant exponent d(L), then L.rootCount a is the number of these balls that contain a root. The balls do not depend on a, so integrating L.rootCount over the Eisenstein polynomials reduces to measuring, ball by ball, the polynomials with a root in that ball.

For the integration itself, each root count is almost everywhere measurable on the Eisenstein region, for any measure on coefficient space. This holds because the Eisenstein region lies in the integer box, where root counts are measurable (IntermediateField.aemeasurable_rootCount).

Main results

• TauCeti.tsum_rootCount_eq_of_separable: at a separable Eisenstein polynomial of degree n, the root counts over σ_K(n) sum to n.
• TauCeti.ae_tsum_rootCount_eq: for additive Haar measure, this identity holds almost everywhere on the Eisenstein region, including in equal characteristic.
• IntermediateField.rootCount_eq_sum_ite_of_eisenstein: for L ∈ σ_K(n), the root count of an Eisenstein polynomial of degree n is the number of balls containing a root, in any disjoint cover of the uniformizers of L by balls of order larger than d(L).
• TauCeti.aemeasurable_rootCount_restrict_eisensteinSet: for L ∈ σ_K(n), the root count in L is almost everywhere measurable on the Eisenstein region.

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, §§2–3.

theorem TauCeti.tsum_rootCount_eq_of_separable {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {a : Fin n → K} {f : Polynomial ↥(ValuativeRel.valuation K).integer} (he : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) (hf : Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f = Polynomial.monicOfCoeff a) (hsep : (Polynomial.monicOfCoeff a).Separable) : ∑' (L : ↑(totallyRamifiedOfDegree K n)), ↑((↑L).rootCount a) = ↑n

The root counts over σ_K(n) sum to n. Let f be an Eisenstein polynomial over 𝒪[K] with image monicOfCoeff a over K, for a : Fin n → K, and assume that monicOfCoeff a is separable. Then ∑_{L ∈ σ_K(n)} L.rootCount a = n: each of the n roots of monicOfCoeff a in the separable closure lies in exactly one member of σ_K(n), the one it generates.

theorem TauCeti.ae_tsum_rootCount_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] : ∀ᵐ (a : Fin n → K) ∂μ.restrict (eisensteinSet K n), ∑' (L : ↑(totallyRamifiedOfDegree K n)), ↑((↑L).rootCount a) = ↑n

Almost everywhere on the Eisenstein region, the root counts over all totally ramified degree-n subextensions sum to n. This also holds in equal characteristic, because the inseparable Eisenstein polynomials have measure zero.

theorem IntermediateField.rootCount_eq_sum_ite_of_eisenstein {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) {a : Fin n → K} {f : Polynomial ↥(ValuativeRel.valuation K).integer} : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) → Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f = TauCeti.Polynomial.monicOfCoeff a → ∀ {r : ℕ}, L.discriminantExponent < r → ∀ (C : Finset ↥(ValuativeRel.valuation ↥L).integer), {x : ↥(ValuativeRel.valuation ↥L).integer | (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) x = 1} ⊆ ⋃ c ∈ C, {x : ↥(ValuativeRel.valuation ↥L).integer | ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (x - c)} → ((↑C).PairwiseDisjoint fun (c : ↥(ValuativeRel.valuation ↥L).integer) => {x : ↥(ValuativeRel.valuation ↥L).integer | ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (x - c)}) → L.rootCount a = ∑ c ∈ C, if ∃ (z : ↥(ValuativeRel.valuation ↥L).integer), (Polynomial.aeval z) f = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (z - c) then 1 else 0

The root count in a counted extension as a sum over balls. Let L ∈ σ_K(n), with its canonical local-field structure, and let f be an Eisenstein polynomial over 𝒪[K] with image monicOfCoeff a over K, for a : Fin n → K. Let C index a family of pairwise disjoint balls v_L(x - c) ≥ r covering the uniformizers of L, of order r larger than the discriminant exponent d(L). Then L.rootCount a is the number of these balls containing a root of f.

theorem TauCeti.aemeasurable_rootCount_restrict_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [OpensMeasurableSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ totallyRamifiedOfDegree K n) : AEMeasurable (fun (a : Fin n → K) => ↑(L.rootCount a)) (μ.restrict (eisensteinSet K n))

The root counts are measurable on the Eisenstein region. For L ∈ σ_K(n) and any measure μ on the coefficient space Fin n → K, the root count a ↦ L.rootCount a is almost everywhere measurable for μ restricted to the Eisenstein region TauCeti.eisensteinSet K n.