Measurable coefficient loci for roots in valuation balls #
For an extension L / K of nonarchimedean local fields, the coefficient vectors of monic
polynomials with a root in a fixed closed ball of 𝒪[L] form a closed set. These sets are
therefore measurable, including at inseparable polynomials. Their indicators are the summands
in the finite ball decomposition of root counts used in Serre's mass-formula integral.
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.isClosed_setOf_exists_aeval_monicOfCoeff_eq_zero_le_addVal
{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]
(n r : ℕ)
(c : ↥(ValuativeRel.valuation L).integer)
:
IsClosed
{a : Fin n → K | ∃ (z : ↥(ValuativeRel.valuation L).integer),
(Polynomial.aeval ↑z) (Polynomial.monicOfCoeff a) = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - c)}
The monic coefficient vectors with a root in a fixed closed valuation ball of the ring of integers of an extension of local fields form a closed set.
theorem
TauCeti.measurableSet_setOf_exists_aeval_monicOfCoeff_eq_zero_le_addVal
{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]
{n : ℕ}
[MeasurableSpace (Fin n → K)]
[OpensMeasurableSpace (Fin n → K)]
(r : ℕ)
(c : ↥(ValuativeRel.valuation L).integer)
:
MeasurableSet
{a : Fin n → K | ∃ (z : ↥(ValuativeRel.valuation L).integer),
(Polynomial.aeval ↑z) (Polynomial.monicOfCoeff a) = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - c)}
The coefficient locus for a root in a fixed closed valuation ball is measurable for any measurable structure containing the open subsets of coefficient space.