A p-adic place for eigenform coefficients and a seed character

Proved

HorizontalPadicL.seededEigenform_padicPlace_exists

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

galois-representationsmodular-formsnumber-theoryp-adic-l-functions

Let $f$ be a new normalized eigenform of positive level and weight at least two, let $p$ be prime, and let $\eta$ be an algebraic Dirichlet character. There is an embedding of the common algebraic coefficient field into $\mathbf C_p$ under which every Fourier coefficient $a_n(f)$ and every value of $\eta$ is $p$ -adically integral.

This supplies the coefficient place at which the residual representation and orderly-prime congruences are evaluated.

Preamble

import Definitions.Def_KN_SeededPrimeGaloisData

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

theorem seededEigenform_padicPlace_exists
    {N k p : ℕ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
    (hnew : IsNewEigenform f) (η : DirichletCharacterWithLevel) :
    Nonempty (SeededEigenformPadicPlaceData (p := p) f η) := by sorry

end HorizontalPadicL

Source

Kriz–Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, §4.3, Lemma 4.14 and Corollary 4.15, pp. 30–31.

View graph