Faithful odd-prime theta elements with norm relations
OpenHorizontalPadicL.seededFiniteThetaElements_exist_with_normRelation_v2dirichlet-charactersmodular-formsnumber-theoryp-adic-l-functions
For odd p, the plus signed modular-symbol theta elements push forward along the quotient maps stored by the faithful character realization. They are integral after the uniform period scaling and satisfy the horizontal one-prime norm relations.
Deprecated. Its comparison hypothesis unnecessarily included the meaningless zero-modulus case. Use replacement node 2de2fc7b-4f50-47fe-8f6f-fc61ea21e109.
Preamble
import Definitions.Def_KN_SeededThetaConstructionV2 set_option autoImplicit false noncomputable section
Formal statement
namespace HorizontalPadicL
/-- For odd `p`, the plus modular-symbol theta elements push forward along the
chosen quotient maps and satisfy the horizontal norm relations. -/
theorem seededFiniteThetaElements_exist_with_normRelation_v2
{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]) (hpodd : p ≠ 2)
(L : SeededHorizontalPrimeDataV2 p ιp f η B)
(characters : SeededHorizontalCharacterRealizationV2 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) :
∃ Θ : SeededFiniteThetaDataV2 L,
Θ.characters = characters ∧ Θ.SatisfiesNormRelations := by
sorry
end HorizontalPadicLSource
Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6, Definition 5.3, Corollary 5.4, Theorem 5.9, Corollary 5.10 and Corollary 5.17.