Fourier coefficients lie in the ring of integers of the coefficient field

Proved

MTT.Eigenform.coeff_mem_ringOfIntegers

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

algebraic-integerscoefficient-fieldsmodular-formsnumber-theory

Let $f$ be an MTT eigenform of positive level and weight at least two, and let $K_f$ be its coefficient field. Every Fourier coefficient $a_n(f)$ , viewed as an element of $K_f$ , lies in the integral closure of $\mathbf Z$ in $K_f$ :

a_n(f)\in\mathcal O_{K_f}.

This upgrades the previously established algebraic integrality of $a_n(f)$ in $\overline{\mathbf Q}$ to literal membership in the integer ring of the canonical coefficient field.

Preamble

import Definitions.Def_MTT_EigenformCoefficientField
import Mathlib.RingTheory.IntegralClosure.Algebra.Basic

set_option autoImplicit false
noncomputable section

Formal statement

/-- Every Fourier coefficient, regarded as an element of the coefficient
field, belongs to its ring of integers. -/
theorem MTT.Eigenform.coeff_mem_ringOfIntegers
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι) (n : ℕ) :
    (⟨f.coeff n, f.coeff_mem_coefficientField n⟩ : f.coefficientField) ∈
      integralClosure ℤ f.coefficientField := by sorry

Source

Standard algebraicity and integrality properties of normalized cuspidal Hecke eigenforms; coefficient-field notation as in Kriz--Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, Section 4, p. 27, https://arxiv.org/pdf/2310.20678

View graph