Construct integral seeded theta elements with their horizontal norm relations

Open

HorizontalPadicL.seededFiniteThetaElements_exist_with_normRelation

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

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

Let f be an even-weight new eigenform, let eta be a primitive even seed character, and choose a p-adic embedding, a density-free orderly-prime datum, a realization of the horizontal characters, and a uniform integral period scale. Assume the algebraic-symbol values agree with the signed classical modular symbols after applying the complex embedding and the chosen periods. Then there exists a system of integral finite-level seeded theta elements, with the prescribed character realization, which satisfies the one-prime horizontal norm relations.

The existential conclusion is essential: the norm relation belongs to the theta elements specifically constructed from modular symbols. It is not a property of every arbitrary value of SeededFiniteThetaData.

Deprecated. It uses the retired unconstrained character-realization interface. Use replacement node 08ffa06b-7342-4fa3-ac2a-b26eb393f5a5.

Preamble

import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- The signed modular-symbol theta elements can be constructed simultaneously
with their one-prime horizontal norm relations.  Combining construction and
compatibility in one conclusion records that the norm relation belongs to the
specific theta elements built from modular symbols, rather than to an arbitrary
value of `SeededFiniteThetaData`.

This is the finite-quotient form of Kriz--Nordentoft, Corollary 3.6, equations
(3.19)--(3.22), followed by the horizontal push-forward of equations
(5.1)--(5.6). -/
theorem seededFiniteThetaElements_exist_with_normRelation
    {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 ∧ Θ.SatisfiesNormRelations := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, Corollary 3.6, equations (3.19)--(3.22), and equations (5.1)--(5.6), https://arxiv.org/pdf/2310.20678

View graph