Horizontal characters realized by primitive Dirichlet characters

Open

HorizontalPadicL.seededHorizontalCharacterRealization_exists

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

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

For a density-free seeded orderly-prime datum, every character of a finite horizontal quotient can be realized by a primitive Dirichlet character supported on the corresponding auxiliary primes. The realization covers every primitive exact-order character supported on finitely many chosen primes and sends the trivial horizontal character to the trivial Dirichlet character.

Retired. This formulation did not relate the assigned Dirichlet character to the given horizontal character through the quotient maps (Z/lZ)^times -> Z/p^(v_p(l-1))Z, and its uniform order bound was false when v_p(l-1) exceeds the selected seed exponent. Use HorizontalPadicL.seededHorizontalCharacterRealization_exists_v2.

Preamble

import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- Characters of the horizontal product are realized by primitive Dirichlet
characters on the chosen auxiliary primes. No density hypothesis is used. -/
theorem seededHorizontalCharacterRealization_exists
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (η : DirichletCharacterWithLevel) (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeDataV2 p ιp f η B) :
    Nonempty (SeededHorizontalCharacterRealization L) := by sorry

end HorizontalPadicL

Source

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

View graph