Documentation

TauCeti.NumberTheory.LocalField.MassFormula.Eisenstein.Region

The Eisenstein region of coefficient space #

Serre's mass formula is proved by integrating over the space of Eisenstein polynomials. A monic polynomial of degree n over a nonarchimedean local field K is identified with its coefficient vector a : Fin n β†’ K, through TauCeti.Polynomial.monicOfCoeff a = X ^ n + βˆ‘ i, a i * X ^ i, and the Eisenstein region TauCeti.eisensteinSet K n is the set of coefficient vectors all of whose entries lie in the open unit ball and whose polynomial has constant term of valuation at least that of every element of valuation below 1. For 0 < n the constant term is the entry a 0, so this says it has the valuation of a uniformizer; for n = 0 the constant term is 1 and the region is all of the one-point space Fin 0 β†’ K. Whenever π’ͺ[K] is a discrete valuation ring, as for a nonarchimedean local field, TauCeti.mem_eisensteinSet_iff_exists_isEisensteinAt identifies these with the coefficient vectors of the polynomials over π’ͺ[K] that are Eisenstein at 𝓂[K] (for n = 0, only the constant polynomial 1, which Mathlib's predicate counts as Eisenstein).

The coefficient space ΞΉ β†’ K carries the additive Haar measure normalized so that the integer box TauCeti.integerBox K ΞΉ = π’ͺ[K] ^ ΞΉ has volume 1. For such a measure, writing q for the cardinality of the residue field, the box whose i-th factor is 𝓂[K] ^ e i has volume q ^ (-βˆ‘ i, e i), since it is the image of the integer box under the diagonal matrix with entries Ο– ^ e i for a uniformizer Ο–. For 0 < n the Eisenstein region is the difference of two such boxes (TauCeti.eisensteinSet_eq_sdiff), so its volume is q ^ (-n) (1 - q⁻¹) (TauCeti.measure_eisensteinSet).

The measure statements assume only left invariance of the measure and the normalization; no product structure on the measure is used.

Main definitions #

Main results #

Implementation notes #

The volume of a box of ideals is MeasureTheory.Measure.measure_univ_pi_image_maximalIdeal_pow, which reads it off the scaling law MeasureTheory.Measure.measure_image_mulVec_integerBox applied to the diagonal matrix Matrix.diagonal fun i ↦ Ο– ^ e i, whose determinant is Ο– ^ βˆ‘ i, e i.

References #

source
def TauCeti.eisensteinSet (K : Type u_1) [Field K] [ValuativeRel K] (n : β„•) :
Set (Fin n β†’ K)

The Eisenstein region in the space Fin n β†’ K of coefficient vectors of monic polynomials of degree n: every coefficient has valuation below 1, and the constant term of monicOfCoeff a has valuation at least that of every element of valuation below 1. For 0 < n the constant term is a 0, which then has the valuation of a uniformizer; for n = 0 it is 1, and the region is the whole one-point space. When π’ͺ[K] is a discrete valuation ring, TauCeti.mem_eisensteinSet_iff_exists_isEisensteinAt identifies these with the coefficient vectors of the polynomials over π’ͺ[K] that are Eisenstein at 𝓂[K].

Instances For
    source
    theorem TauCeti.mem_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] {n : β„•} {a : Fin n β†’ K} :
    a ∈ eisensteinSet K n ↔ (βˆ€ (i : Fin n), (ValuativeRel.valuation K) (a i) < 1) ∧ βˆ€ (y : K), (ValuativeRel.valuation K) y < 1 β†’ (ValuativeRel.valuation K) y ≀ (ValuativeRel.valuation K) ((Polynomial.monicOfCoeff a).coeff 0)

    Membership in the Eisenstein region, unfolded.

    source
    theorem TauCeti.eisensteinSet_subset_integerBox {K : Type u_1} [Field K] [ValuativeRel K] (n : β„•) :
    eisensteinSet K n βŠ† integerBox K (Fin n)

    The Eisenstein region lies in the integer box: its coefficients are integral.

    source
    theorem TauCeti.mem_eisensteinSet_iff_exists_isEisensteinAt {K : Type u_1} [Field K] [ValuativeRel K] [IsDiscreteValuationRing β†₯(ValuativeRel.valuation K).integer] {n : β„•} {a : Fin n β†’ K} :
    a ∈ eisensteinSet K n ↔ βˆƒ (f : Polynomial β†₯(ValuativeRel.valuation K).integer), Polynomial.map (algebraMap (β†₯(ValuativeRel.valuation K).integer) K) f = Polynomial.monicOfCoeff a ∧ f.IsEisensteinAt (IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer)

    The Eisenstein region is the set of Eisenstein polynomials: a coefficient vector lies in eisensteinSet K n exactly when it is the coefficient vector of a polynomial over π’ͺ[K] that is Eisenstein at 𝓂[K].

    source
    theorem TauCeti.irreducible_monicOfCoeff_of_mem_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [IsDiscreteValuationRing β†₯(ValuativeRel.valuation K).integer] {n : β„•} (hn : 0 < n) {a : Fin n β†’ K} (ha : a ∈ eisensteinSet K n) :
    Irreducible (Polynomial.monicOfCoeff a)

    An Eisenstein coefficient vector of positive degree defines an irreducible polynomial over the base field.

    source
    theorem TauCeti.eisensteinSet_eq_sdiff {K : Type u_1} [Field K] [ValuativeRel K] [IsDiscreteValuationRing β†₯(ValuativeRel.valuation K).integer] {n : β„•} (hn : 0 < n) :
    eisensteinSet K n = (Set.univ.pi fun (x : Fin n) => Subtype.val '' ↑(IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer)) \ Set.univ.pi fun (i : Fin n) => Subtype.val '' ↑(IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ Function.update (fun (x : Fin n) => 1) ⟨0, hn⟩ 2 i)

    The Eisenstein region as a difference of boxes: for 0 < n, it is the box 𝓂[K] ^ n minus the box whose constant coordinate lies in 𝓂[K] ^ 2 and whose other coordinates lie in 𝓂[K].

    source
    theorem TauCeti.measurableSet_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} [MeasurableSpace (Fin n β†’ K)] [OpensMeasurableSpace (Fin n β†’ K)] :
    MeasurableSet (eisensteinSet K n)

    The Eisenstein region is measurable.

    source
    theorem TauCeti.measure_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} (hn : 0 < n) [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : MeasureTheory.Measure (Fin n β†’ K)) [ΞΌ.IsAddLeftInvariant] (hΞΌ : ΞΌ (integerBox K (Fin n)) = 1) :
    ΞΌ (eisensteinSet K n) = 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)) ^ n * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)))

    The volume of the Eisenstein region: for a left-invariant measure on Fin n β†’ K normalized on the integer box, the Eisenstein region has volume q ^ (-n) (1 - q⁻¹) for 0 < n, where q = Nat.card 𝓀[K].

    source
    theorem TauCeti.measure_eisensteinSet_lt_top {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} [MeasurableSpace (Fin n β†’ K)] (ΞΌ : MeasureTheory.Measure (Fin n β†’ K)) [MeasureTheory.IsFiniteMeasureOnCompacts ΞΌ] :
    μ (eisensteinSet K n) < ⊀

    The Eisenstein region has finite volume for every measure that is finite on compact sets, since it lies in the compact integer box.

    source
    theorem TauCeti.measure_eisensteinSet_pos {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} [MeasurableSpace (Fin n β†’ K)] [BorelSpace (Fin n β†’ K)] (ΞΌ : MeasureTheory.Measure (Fin n β†’ K)) [ΞΌ.IsAddHaarMeasure] :
    0 < ΞΌ (eisensteinSet K n)

    The Eisenstein region has positive volume for every additive Haar measure, not only for the one normalized on the integer box.