Counting roots of an Eisenstein polynomial in balls

Let L / K be a finite separable extension of nonarchimedean local fields and g an Eisenstein polynomial over 𝒪[K] of degree [L : K]. Every root z of g in 𝒪[L] generates L over K (TauCeti.adjoin_eq_top_of_eisenstein_of_natDegree_eq_finrank), so it is a uniformizer of L, and the order of g'(z) is the different exponent d of L / K. Consequently, if the uniformizers of L are covered by a finite family of pairwise disjoint balls of order r > d, each ball contains at most one root of g, and the number of roots of g in 𝒪[L] is the number of balls containing a root. Such a family of balls exists for every order r ≥ 2, by TauCeti.exists_finset_addVal_eq_biUnion.

The point of this count is that the family of balls is fixed once and for all, independently of g: the root count of every Eisenstein polynomial of degree [L : K] becomes a finite sum of indicators of the same balls. Integrating the root count over the Eisenstein polynomials thus reduces to measuring, for each ball, the polynomials having a root in it.

Main results

• TauCeti.card_roots_map_eq_sum_ite_of_eisenstein: the number of roots in 𝒪[L] of an Eisenstein polynomial of degree [L : K] is the number of balls of a disjoint cover of the uniformizers by balls of order larger than the different exponent that contain a root.

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

theorem TauCeti.card_roots_map_eq_sum_ite_of_eisenstein {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] [Algebra.IsSeparable K L] {g : Polynomial ↥(ValuativeRel.valuation K).integer} (hg : g.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) (hdeg : g.natDegree = Module.finrank K L) {r : ℕ} (hr : differentExponent K L < r) (C : Finset ↥(ValuativeRel.valuation L).integer) (hcover : {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)}) (hdisj : (↑C).PairwiseDisjoint fun (c : ↥(ValuativeRel.valuation L).integer) => {x : ↥(ValuativeRel.valuation L).integer | ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (x - c)}) : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) g).roots.card = ∑ c ∈ C, if ∃ (z : ↥(ValuativeRel.valuation L).integer), (Polynomial.aeval z) g = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - c) then 1 else 0

Root counts of Eisenstein polynomials as sums over balls. Let g be an Eisenstein polynomial over 𝒪[K] of degree [L : K], and 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 different exponent of L / K. Then the number of roots of g in 𝒪[L], counted with multiplicity, is the number of these balls that contain a root of g.