Counting the balls in a valuation sphere

In a discrete valuation ring with finite residue field of cardinality q, the sphere of order s contains exactly q ^ (r - s) - q ^ (r - (s + 1)) congruence classes modulo the r-th power of the maximal ideal, for s < r. Consequently every disjoint partition of this sphere into balls of order r has that many members. For the uniformizers (s = 1) these are the finite partitions used to integrate polynomial root counts: the number of balls, multiplied by the common measure of a local fibre, gives the integral. Equivalently, if each ball of order r is given mass q ^ (-r), the partition has total mass q ^ (-s) (1 - q⁻¹), independently of r.

The count is purely algebraic and requires neither completeness nor a topology. It follows by subtracting the numbers of classes in two successive ideal powers, computed using the third isomorphism theorem and the cardinality of the quotient by an ideal power.

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.ncard_image_quotient_mk_maximalIdeal_pow {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Finite (IsLocalRing.ResidueField A)] {s r : ℕ} (hsr : s ≤ r) : (⇑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal A ^ r)) '' ↑(IsLocalRing.maximalIdeal A ^ s)).ncard = Nat.card (IsLocalRing.ResidueField A) ^ (r - s)

The image of an ideal power modulo a deeper ideal power has q ^ (r - s) elements.

theorem TauCeti.ncard_image_quotient_mk_addVal_eq {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Finite (IsLocalRing.ResidueField A)] {s r : ℕ} (hsr : s < r) : (⇑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal A ^ r)) '' {x : A | (IsDiscreteValuationRing.addVal A) x = ↑s}).ncard = Nat.card (IsLocalRing.ResidueField A) ^ (r - s) - Nat.card (IsLocalRing.ResidueField A) ^ (r - (s + 1))

There are q ^ (r - s) - q ^ (r - (s + 1)) classes of valuation exactly s modulo 𝓂 ^ r. The assumption s < r makes valuation s independent of the representative.

theorem TauCeti.card_finset_of_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) (hcover : {x : A | (IsDiscreteValuationRing.addVal A) x = ↑s} = ⋃ c ∈ C, {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}) (hdisj : (↑C).PairwiseDisjoint fun (c : A) => {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}) : C.card = Nat.card (IsLocalRing.ResidueField A) ^ (r - s) - Nat.card (IsLocalRing.ResidueField A) ^ (r - (s + 1))

Every disjoint partition of the sphere of order s into balls of order r > s has the same cardinality, computed from the residue cardinality.

theorem TauCeti.card_finset_div_pow_of_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) (hcover : {x : A | (IsDiscreteValuationRing.addVal A) x = ↑s} = ⋃ c ∈ C, {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}) (hdisj : (↑C).PairwiseDisjoint fun (c : A) => {x : A | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)}) : ↑C.card / ↑(Nat.card (IsLocalRing.ResidueField A)) ^ r = 1 / ↑(Nat.card (IsLocalRing.ResidueField A)) ^ s * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField A)))

Every disjoint partition of the sphere of order s into balls of order r > s has total mass q ^ (-s) (1 - q⁻¹) when each ball has mass q ^ (-r), where q is the residue cardinality.