Scaling of Haar measure on ι → K under integral matrices #
Let K be a nonarchimedean local field with residue field of cardinality q, and let A be a
square matrix over 𝒪[K] whose determinant is associated to ϖ ^ k for a uniformizer ϖ.
Acting on ι → K by mulVec, A multiplies Haar measure by q ^ (-k). This is the
nonarchimedean analogue of Mathlib's MeasureTheory.Measure.addHaar_image_linearMap, where the
factor is |det| for a real vector space.
The proof runs through the lattice index. The image under A of the integer box
∏ i, 𝒪[K] is a subgroup of index q ^ k in it
(Matrix.card_quotient_range_mulVecLin_eq_pow), so the box is the disjoint union of q ^ k
translates of that image, and Mathlib's MeasureTheory.AddSubgroup.index_mul_measure turns this
into the measure identity. On a translate of a scaled box — that is, on a ball of ι → K — the
same identity holds for every left-invariant measure, with no regularity hypothesis. For a general
set the measure s ↦ μ (A '' s) is again a Haar measure, so by uniqueness of Haar measure it is a
constant multiple of μ, and the box computes the constant; Haar measure on ι → K is
automatically regular, since ι → K is second countable and locally compact.
Specializing to diagonal matrices gives the volume of a box of ideals: the box whose i-th factor
is 𝓂[K] ^ e i is the image of the integer box under the diagonal matrix with entries ϖ ^ e i,
whose determinant is ϖ ^ ∑ i, e i, so it has q ^ (-∑ i, e i) times the measure of the box.
The topological box lemmas apply to valuative fields without local compactness; compactness of the
integer box only requires compactness of 𝒪[K].
These volumes are the change of variables in Serre's proof of his mass formula for totally
ramified extensions, where A is the matrix of multiplication by an element of the ring of
integers of an extension of K in an integral basis and k is the valuation of its norm.
Main definitions #
TauCeti.integerBox K ι: the integer box∏ i, 𝒪[K]inι → K.TauCeti.scaledIntegerBox ι ϖ k: the scaled integer box{x | ϖ ^ k • x ∈ integerBox K ι}, an additive subgroup ofι → K.
Main results #
TauCeti.isOpen_integerBox,TauCeti.isCompact_integerBox: the integer box is open and compact.TauCeti.isCompact_scaledIntegerBox,TauCeti.exists_mem_scaledIntegerBox: the scaled integer boxes are compact, and for a uniformizerϖthey exhaustι → K.TauCeti.univ_pi_image_maximalIdeal_pow_subset,TauCeti.isClosed_univ_pi_image_maximalIdeal_pow,TauCeti.measurableSet_univ_pi_image_maximalIdeal_pow: boxes of ideal powers shrink as the exponents grow, and are closed and measurable.MeasureTheory.Measure.measure_image_mulVec_integerBox: for a left-invariantμ, the image of the integer box has measureq ^ (-k)times that of the box.MeasureTheory.Measure.measure_image_mulVec_vadd_smul_integerBox: the same for every ballx +ᵥ c • ∏ i, 𝒪[K]withc ≠ 0.MeasureTheory.Measure.measure_univ_pi_image_maximalIdeal_pow: for a left-invariantμ, the box with factors𝓂[K] ^ e ihasq ^ (-∑ i, e i)times the volume of the integer box.MeasureTheory.Measure.measure_integerBox_inter_coord_eq_zero: a coordinate hyperplane inside an integer box of finite measure is null.MeasureTheory.Measure.addHaar_image_mulVec: for a Haar measureμ,μ (A '' s) = q ^ (-k) * μ sfor every sets.
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.
The integer box ∏ i, 𝒪[K] of ι → K, on which Haar measure on ι → K is normalized.
Instances For
Membership in the integer box: every coordinate is integral.
The integer box is the product of copies of 𝒪[K].
Boxes of ideal powers shrink as the exponents grow.
The scaled integer box {x | ϖ ^ k • x ∈ integerBox K ι}, an additive subgroup of
ι → K.
Instances For
Membership in a scaled integer box, coordinate by coordinate.
A scaled integer box is the preimage of the integer box under multiplication by ϖ ^ k.
For a uniformizer ϖ and a finite type ι, the scaled integer boxes exhaust ι → K: a power
of ϖ clears the denominators of the coordinates of x, since K is the localization of 𝒪[K]
away from ϖ.
The integer box is open.
If 𝒪[K] is compact, its integer box is compact for any index type.
If 𝒪[K] is compact, a scaled integer box with nonzero scale is compact: it is the preimage
of the integer box under a homeomorphism.
A box of ideal powers is closed.
A box of ideal powers is measurable.
The scaling law on the integer box. If the determinant of a square matrix A over
𝒪[K] is associated to ϖ ^ k for a uniformizer ϖ, then for every left-invariant measure on
ι → K, the image of the integer box ∏ i, 𝒪[K] under A has q ^ (-k) times the measure of
the box, where q = Nat.card 𝓀[K].
The volume of a box of ideals: for a left-invariant measure on ι → K, the box whose
i-th factor is 𝓂[K] ^ e i has q ^ (-∑ i, e i) times the volume of the integer box, where
q = Nat.card 𝓀[K].
A coordinate hyperplane inside the integer box is null for a left-invariant measure whose integer box has finite measure.
The scaling law on balls. If the determinant of a square matrix A over 𝒪[K] is
associated to ϖ ^ k for a uniformizer ϖ, then for every left-invariant measure on ι → K,
the image under A of the ball x +ᵥ c • ∏ i, 𝒪[K] (with c ≠ 0) has q ^ (-k) times the
measure of the ball, where q = Nat.card 𝓀[K].
The scaling law for Haar measure. If the determinant of a square matrix A over 𝒪[K]
is associated to ϖ ^ k for a uniformizer ϖ, then for every additive Haar measure μ
on ι → K and every set s, μ (A '' s) = q ^ (-k) * μ s, where q = Nat.card 𝓀[K]. This is
the nonarchimedean analogue of MeasureTheory.Measure.addHaar_image_linearMap.