Full support identifies the level character with its primitive realization

Proved

HorizontalPadicL.fullSupport_atLevel_apply_eq_realized

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

dirichlet-charactersmodular-formsmodular-symbolsp-adic-l-functions

When the conductor of the primitive realization is the entire selected support modulus, the level character used in the horizontal quotient agrees with that primitive character on every unit. Integer representatives are used to avoid transports between equal ZMod levels.

Preamble

import Definitions.Def_KN_SeededInverseThetaSystem

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- If a horizontal character uses its full conductor, then the full-level
character used in the quotient construction agrees, on units, with its
primitive realization.  The formulation on integer representatives avoids
dependent transports between equal `ZMod` levels. -/
theorem fullSupport_atLevel_apply_eq_realized
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
    {η : DirichletCharacterWithLevel}
    {L : SeededHorizontalPrimeDataV3 p ιp f η B}
    (R : SeededHorizontalCharacterRealizationV3 L)
    (χ : HorizontalCharacter p L.exponent)
    (hfull : (R.realized χ).2.conductor = L.supportModulus χ.support)
    (u : (ZMod (L.supportModulus χ.support))ˣ) :
    R.atLevel χ u.val.val = (R.realized χ).2 u.val.val := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6 and Corollary 5.4; standard Dirichlet-character and modular-symbol identities.

View graph