Faithful realization of horizontal characters exists

Proved

HorizontalPadicL.seededHorizontalCharacterRealization_exists_v2

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

dirichlet-charactersnumber-theoryp-adic-l-functions

For every seeded horizontal prime datum, choose the cyclic quotient maps from the unit groups at the auxiliary primes. Every finite C_p-valued horizontal character is the pullback of an algebraic Dirichlet character along their product. Primitive reduction preserves the character order; the empty-support character becomes the trivial Dirichlet character; and every primitive p-power-order Dirichlet character supported on finitely many selected primes occurs. No false upper bound by the seed exponent is imposed on arbitrary horizontal characters.

Preamble

import Definitions.Def_KN_SeededHorizontalCharacterRealizationV2

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- The quotient maps `(Z/ℓₙZ)ˣ ↠ Z/p^(vₚ(ℓₙ-1))Z` can be chosen so that
every finite-order horizontal character is the pullback of an algebraic
Dirichlet character.  Primitive reduction preserves its order, and every
primitive `p`-power-order Dirichlet character supported on the selected primes
arises in this way.

This is the faithful replacement for
`seededHorizontalCharacterRealization_exists`: its conclusion includes the
actual pullback equation through the chosen quotient maps. -/
theorem seededHorizontalCharacterRealization_exists_v2
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
    {η : DirichletCharacterWithLevel}
    (L : SeededHorizontalPrimeDataV2 p ιp f η B) :
    ∃ R : SeededHorizontalCharacterRealizationV2 L,
      R.HasExpectedProperties := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, equation (5.1), Corollary 5.4.

View graph