Prove2Me

Integral finite-level seeded theta elements

Open
HorizontalPadicL.seededFiniteThetaElements_exist

by davidloeffler · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsmodular-symbolsnumber-theoryp-adic-l-functions

The signed modular symbols, the simultaneous character realization, and one uniform period denominator define integral theta elements in every finite horizontal group algebra, together with their Euler transition factors.

Preamble
import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section
Formal statement
namespace HorizontalPadicL

/-- The signed modular symbols define integral finite-level theta elements after
the single denominator clearing supplied by the period lattice. -/
theorem seededFiniteThetaElements_exist
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (P : MTT.Periods k ι f.form) (η : DirichletCharacterWithLevel)
    (hηprim : η.2.IsPrimitive) (hηeven : η.2 (-1) = 1)
    (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (characters : SeededHorizontalCharacterRealization L)
    (scale : IntegralPeriodScale f ιp P)
    (hcomparison : ∀ s j a m, j ≤ k - 2 →
      ι (MTT.algebraicSymbol P s j a m) * P.omega s =
        signedModularSymbol f.form s j a m) :
    ∃ Θ : SeededFiniteThetaData L, Θ.characters = characters := by sorry

end HorizontalPadicL
Source
Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Sections 3 and 5.

View graph