Prove2Me

Prime Hecke eigenvalues are algebraic integers

Proved
MTT.Eigenform.heckeEigenvalue_isIntegral

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

algebraic-integerscohomologymodular-formsnumber-theory

For a normalized algebraic Hecke eigenform f of positive level and weight at least two, the eigenvalue a_ell(f) is integral over Z for every prime ell.

The intended reduction uses the nonzero finitely generated period-evaluation lattice stable under multiplication by a_ell(f), and the standard finite-module criterion for integrality.

Preamble
import Definitions.Def_MTT_Arithmetic
import Mathlib.RingTheory.IntegralClosure.Algebra.Basic

set_option autoImplicit false
noncomputable section
Formal statement
theorem MTT.Eigenform.heckeEigenvalue_isIntegral
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
    (l : ℕ) (hl : l.Prime) :
    IsIntegral ℤ (f.coeff l) := by
  sorry
Source
Standard integrality criterion for an element preserving a nonzero faithful finite lattice, applied to the integral parabolic-cohomology lattice.

View graph