The coefficient field of an eigenform is a number field

Proved

MTT.Eigenform.coefficientField_finiteDimensional

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

coefficient-fieldshecke-operatorsmodular-formsnumber-theory

Let $N>0$ and $k\ge2$ , and let $f$ be a normalized algebraic cuspidal Hecke eigenform of level $N$ and weight $k$ . Its coefficient field

K_f=\mathbf Q\bigl(a_n(f),\varepsilon_f(a):n\ge0,\ a\in\mathbf Z/N\mathbf Z\bigr) \subset\overline{\mathbf Q}

is finite-dimensional over $\mathbf Q$ . Thus all Fourier coefficients, Hecke eigenvalues, and nebentype values lie in one common number field, rather than merely being algebraic individually.

This provides the uniform coefficient field needed to choose a place above $p$ and form the residual Galois representation of $f$ .

Preamble

import Definitions.Def_MTT_EigenformCoefficientField

set_option autoImplicit false
noncomputable section

Formal statement

/-- The Fourier coefficients and nebentype values of an MTT eigenform generate
a single number field inside `MTT.Qbar`. -/
theorem MTT.Eigenform.coefficientField_finiteDimensional
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι) :
    FiniteDimensional ℚ f.coefficientField := by sorry

Source

The standard coefficient-field theorem for normalized cuspidal Hecke eigenforms; see Kriz--Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, Section 4, p. 27, https://arxiv.org/pdf/2310.20678

View graph