Documentation

TauCeti.NumberTheory.LocalField.IntegerRing.Volume

Volumes of balls of π’ͺ[L] in uniformizer coordinates #

Let L/K be an extension of nonarchimedean local fields with ramification index n = e(L/K), let Ο– be a uniformizer of L, and write q = Nat.card 𝓀[K]. A coefficient vector c : Fin n β†’ π’ͺ[K] represents the element βˆ‘ i, c i * Ο– ^ i of π’ͺ[L]. Equip the coefficient space Fin n β†’ K with a left-invariant measure normalized on the integer box. This file computes the volume of the coefficient vectors representing the elements of a valuation ball of π’ͺ[L]: the ball of radius r has volume q ^ (-r).

The ball is a box: by orthogonality of the terms c i * Ο– ^ i, whose valuations are distinct modulo n, the coefficient vectors with r ≀ v_L(βˆ‘ i, c i * Ο– ^ i) are those with c i ∈ 𝓂[K] ^ ((r - i) ⌈/βŒ‰ n) (TauCeti.le_addVal_sum_algebraMap_mul_pow_iff_of_irreducible). That box has volume q ^ (-βˆ‘ i, (r - i) ⌈/βŒ‰ n) (MeasureTheory.Measure.measure_univ_pi_image_maximalIdeal_pow), and the exponent is r by Hermite's identity (Nat.sum_range_sub_ceilDiv).

When L/K is totally ramified, the powers 1, Ο–, …, Ο– ^ (n - 1) form a basis of π’ͺ[L] over π’ͺ[K], so every ball y + 𝓂[L] ^ r of π’ͺ[L] is a translate of the ball around 0 in these coordinates and has the same volume. Two consequences are recorded: the sphere v_L(x - y) = r has volume q ^ (-r) (1 - q⁻¹), and so, at y = 0 and r = 1, the uniformizers of L have volume q⁻¹ (1 - q⁻¹); and, for monic polynomials g of degree n over π’ͺ[K] identified with their lower coefficients through TauCeti.Polynomial.monicOfCoeff, the condition r ≀ v_L(g(Ο–)) cuts out a set of volume q ^ (-r), since g(Ο–) - Ο– ^ n is the element with coordinates the lower coefficients of g.

These volumes are the measure computations in Serre's proof of his mass formula: in the local fibre count, the monic polynomials with a root close to a given uniformizer form a set of the second kind, and the uniformizers of L are partitioned into balls of the first kind.

Main results #

References #

source
theorem TauCeti.image_setOf_le_addVal_sum_algebraMap_mul_pow_eq_pi {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} (hΟ– : Irreducible Ο–) (hn : n ≀ ramificationIndex K L) (r : β„•) :
(fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) (βˆ‘ i : Fin n, (algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) (c i) * Ο– ^ ↑i)} = Set.univ.pi fun (i : Fin n) => Subtype.val '' ↑(IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ ((r - ↑i) ⌈/βŒ‰ ramificationIndex K L))

Balls in uniformizer coordinates are boxes. For a uniformizer Ο– of L and n ≀ e(L/K), the coefficient vectors c : Fin n β†’ π’ͺ[K] with r ≀ v_L(βˆ‘ i, c i * Ο– ^ i) form, in Fin n β†’ K, the box whose i-th factor is 𝓂[K] ^ ((r - i) ⌈/βŒ‰ e(L/K)).

source
theorem TauCeti.IsTotallyRamified.measurableSet_image_setOf_le_addVal_sum_algebraMap_mul_pow_sub {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (h : IsTotallyRamified K L) (hΟ– : Irreducible Ο–) (hn : ramificationIndex K L = n) (y : β†₯(ValuativeRel.valuation L).integer) (r : β„•) :
MeasurableSet ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) (βˆ‘ i : Fin n, (algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) (c i) * Ο– ^ ↑i - y)})

In a totally ramified extension, the ball of radius r around y ∈ π’ͺ[L], in uniformizer coordinates, is a measurable subset of Fin n β†’ K, where n = e(L/K).

source
theorem TauCeti.IsTotallyRamified.measurableSet_image_setOf_le_addVal_aeval_monicOfCoeff {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (h : IsTotallyRamified K L) (hΟ– : Irreducible Ο–) (hn : ramificationIndex K L = n) (r : β„•) :
MeasurableSet ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) ((Polynomial.aeval Ο–) (Polynomial.monicOfCoeff c))})

In a totally ramified extension, with n = e(L/K), the monic polynomials g of degree n over π’ͺ[K] with r ≀ v_L(g(Ο–)), identified with their lower coefficients, form a measurable subset of Fin n β†’ K.

source
theorem MeasureTheory.Measure.measure_image_setOf_le_addVal_sum_algebraMap_mul_pow {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : Measure (Fin n β†’ K)) [ΞΌ.IsAddLeftInvariant] (hΞΌ : ΞΌ (TauCeti.integerBox K (Fin n)) = 1) (hΟ– : Irreducible Ο–) (hn : TauCeti.ramificationIndex K L = n) (r : β„•) :
ΞΌ ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) (βˆ‘ i : Fin n, (algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) (c i) * Ο– ^ ↑i)}) = 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)) ^ r

The volume of a ball in uniformizer coordinates. For a uniformizer Ο– of L and n = e(L/K), and a left-invariant measure on Fin n β†’ K normalized on the integer box, the coefficient vectors c : Fin n β†’ π’ͺ[K] with r ≀ v_L(βˆ‘ i, c i * Ο– ^ i) have volume q ^ (-r), where q = Nat.card 𝓀[K].

source
theorem MeasureTheory.Measure.measure_image_setOf_le_addVal_sum_algebraMap_mul_pow_sub {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : Measure (Fin n β†’ K)) [ΞΌ.IsAddLeftInvariant] (h : TauCeti.IsTotallyRamified K L) (hΞΌ : ΞΌ (TauCeti.integerBox K (Fin n)) = 1) (hΟ– : Irreducible Ο–) (hn : TauCeti.ramificationIndex K L = n) (y : β†₯(ValuativeRel.valuation L).integer) (r : β„•) :
ΞΌ ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) (βˆ‘ i : Fin n, (algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) (c i) * Ο– ^ ↑i - y)}) = 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)) ^ r

The volume of a ball of π’ͺ[L]. In a totally ramified extension L/K with uniformizer Ο– and n = e(L/K) = [L : K], and for a left-invariant measure on Fin n β†’ K normalized on the integer box, the coefficient vectors c : Fin n β†’ π’ͺ[K] with r ≀ v_L(βˆ‘ i, c i * Ο– ^ i - y) have volume q ^ (-r), where q = Nat.card 𝓀[K], for every center y ∈ π’ͺ[L].

source
theorem MeasureTheory.Measure.measure_image_setOf_addVal_sum_algebraMap_mul_pow_sub_eq {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : Measure (Fin n β†’ K)) [ΞΌ.IsAddLeftInvariant] (h : TauCeti.IsTotallyRamified K L) (hΞΌ : ΞΌ (TauCeti.integerBox K (Fin n)) = 1) (hΟ– : Irreducible Ο–) (hn : TauCeti.ramificationIndex K L = n) (y : β†₯(ValuativeRel.valuation L).integer) (r : β„•) :
ΞΌ ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) (βˆ‘ i : Fin n, (algebraMap β†₯(ValuativeRel.valuation K).integer β†₯(ValuativeRel.valuation L).integer) (c i) * Ο– ^ ↑i - y) = ↑r}) = 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)) ^ r * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)))

The volume of a sphere of π’ͺ[L]. In a totally ramified extension L/K with uniformizer Ο– and n = e(L/K) = [L : K], and for a left-invariant measure on Fin n β†’ K normalized on the integer box, the coefficient vectors c : Fin n β†’ π’ͺ[K] with v_L(βˆ‘ i, c i * Ο– ^ i - y) = r have volume q ^ (-r) (1 - q⁻¹), where q = Nat.card 𝓀[K], for every center y ∈ π’ͺ[L]. At y = 0 and r = 1 these are the coordinates of the uniformizers of L.

source
theorem MeasureTheory.Measure.measure_image_setOf_le_addVal_aeval_monicOfCoeff {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] {Ο– : β†₯(ValuativeRel.valuation L).integer} {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : Measure (Fin n β†’ K)) [ΞΌ.IsAddLeftInvariant] (h : TauCeti.IsTotallyRamified K L) (hΞΌ : ΞΌ (TauCeti.integerBox K (Fin n)) = 1) (hΟ– : Irreducible Ο–) (hn : TauCeti.ramificationIndex K L = n) (r : β„•) :
ΞΌ ((fun (c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n β†’ β†₯(ValuativeRel.valuation K).integer | ↑r ≀ (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation L).integer) ((Polynomial.aeval Ο–) (TauCeti.Polynomial.monicOfCoeff c))}) = 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)) ^ r

The volume of the monic polynomials with a small value at a uniformizer. In a totally ramified extension L/K with uniformizer Ο– and n = e(L/K) = [L : K], and for a left-invariant measure on Fin n β†’ K normalized on the integer box, the monic polynomials g of degree n over π’ͺ[K] with r ≀ v_L(g(Ο–)), identified with their lower coefficients, have volume q ^ (-r), where q = Nat.card 𝓀[K].