Supported p-power characters are realized horizontally

Proved

HorizontalPadicL.SeededHorizontalCharacterRealizationV2.realizes_supported_pPower_character

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

dirichlet-charactersnumber-theoryp-adic-l-functions

Let R be a faithful realization of horizontal characters using the maximal p-power quotients of the unit groups at the selected auxiliary primes. Every primitive Dirichlet character of p-power order whose conductor divides a finite product of selected primes is the primitive character realized by some finite horizontal character.

Preamble

import Definitions.Def_KN_SeededHorizontalCharacterRealizationV2

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- Every primitive `p`-power-order Dirichlet character supported on finitely
many selected horizontal primes is obtained from the corresponding horizontal
finite quotient. -/
theorem SeededHorizontalCharacterRealizationV2.realizes_supported_pPower_character
    {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)
    (ψ : DirichletCharacterWithLevel)
    (hprimitive : ψ.2.IsPrimitive)
    (horder : ∃ a : ℕ, orderOf ψ.2 = p ^ a)
    (hsupport : ∃ A : Finset ℕ,
      ψ.2.conductor ∣ L.supportModulus A) :
    ∃ χ : HorizontalCharacter p L.exponent,
      R.realized χ = ψ := 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