Finite ball partitions and root counts

Over a discrete valuation ring with finite residue field, every valuation sphere of order s is a finite disjoint union of balls of order r > s, with centres on that sphere. In particular, the uniformizers admit such a partition whenever 2 ≤ r.

If the roots of a polynomial lie on a sphere and the derivative order at each root is less than r, every ball in a partition of order r contains at most one root, and all rational roots are simple. Its root count is consequently the sum of the indicators of the balls containing a root. The partition can be chosen once for an entire family of polynomials; only the derivative bound and the location of the roots vary with the polynomial. This is the finite sum used to integrate root counts by local fibre computations.

No completeness or topology is needed for either assertion.

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.exists_finset_addVal_eq_biUnion {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Finite (IsLocalRing.ResidueField A)] {s r : ℕ} (hsr : s < r) : ∃ (C : Finset A), (∀ c ∈ C, (IsDiscreteValuationRing.addVal A) c = ↑s) ∧ {x : A | (IsDiscreteValuationRing.addVal A) x = ↑s} = ⋃ c ∈ C, {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)} ∧ (↑C).PairwiseDisjoint fun (c : A) => {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}

A valuation sphere is a finite disjoint union of smaller balls, with centres on the sphere. For s = 1, this partitions the uniformizers. The same partition is available independently of any polynomial whose roots will subsequently be counted.

theorem Polynomial.card_roots_eq_sum_ite_of_addVal_lt {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (F : Polynomial A) (C : Finset A) {r : ℕ} (hcover : ∀ x ∈ F.roots, ∃ c ∈ C, ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)) (hdisj : (↑C).PairwiseDisjoint fun (c : A) => {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}) (hder : ∀ x ∈ F.roots, (IsDiscreteValuationRing.addVal A) (eval x (derivative F)) < ↑r) : F.roots.card = ∑ c ∈ C, if ∃ x ∈ F.roots, ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c) then 1 else 0

Count roots by a finite disjoint family of balls covering them. If the derivative order at each root is smaller than the ball order, each occupied ball contributes exactly one root. The derivative bound also excludes repeated rational roots, so no separability hypothesis is needed.