The coefficient field of a newform is a number field

For a normalised full eigenform f of weight k ≥ 2, every Fourier coefficient a_n(f) is an algebraic integer. Consequently, the coefficient field ℚ(a_n(f) : n ≥ 1) of a newform is a number field.

The integral input is the finiteness over ℤ of the algebra generated by the Hecke operators on S_k(Γ₁(N)). A newform is an eigenvector of T_p with eigenvalue a_p at every prime p, the primes dividing the level included, so it is a joint eigenvector of the ℤ-algebra generated by the prime-index operators. Its eigenvalues form a ring homomorphism from that algebra to ℂ. The image is a finitely generated ℤ-module of algebraic integers containing every a_p. The coefficients at the other indices are reached through the Hecke recurrences from the a_p and the nebentypus values, which are roots of unity.

Weight one is not covered: the finiteness of the Hecke algebra comes from modular symbols, which carry the weight-k coefficient system Sym^{k−2} and so exist only in weight at least two.

Main results

• HeckeRing.GL2.Eigenform.isIntegral_qExpansion_coeff: the Fourier coefficients of a normalised full eigenform of weight at least two are algebraic integers.
• HeckeRing.GL2.Newform.isIntegral_qExpansion_coeff: the newform specialisation.
• TauCeti.numberField_CoefficientField: the coefficient field of a newform of weight at least two is a number field.

Provenance

The same statements are proved in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB), projects/LeanModularForms/LeanModularForms/Labels/NewformOrbit.lean, as coeffSeq_isIntegral and coeffField_numberField_of_two_le, by the same route through the eigenvalue homomorphism of a ℤ-finite Hecke algebra.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3.
• T. Miyake, Modular forms, Section 4.5.

noncomputable def HeckeRing.GL2.Eigenform.eigenvalueHom {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) : ↥(TauCeti.heckeTCuspPrimeAlgebra N k) →ₐ[ℤ] ℂ

The eigenvalue homomorphism of a normalised full eigenform on the prime-index Hecke algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HeckeRing.GL2.Eigenform.eigenvalueHom_apply {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (T : ↥(TauCeti.heckeTCuspPrimeAlgebra N k)) : (f.eigenvalueHom h₁) T = (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑(↑T f.toCuspForm))

The eigenvalue of an operator in the prime-index Hecke algebra on a normalised full eigenform is the first Fourier coefficient of its image.

theorem HeckeRing.GL2.Eigenform.heckeTCuspPrimeAlgebra_apply_eq_eigenvalueHom_smul {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (T : ↥(TauCeti.heckeTCuspPrimeAlgebra N k)) : ↑T f.toCuspForm = (f.eigenvalueHom h₁) T • f.toCuspForm

A normalised full eigenform is an eigenvector of every operator in the prime-index Hecke algebra, with eigenvalue given by its eigenvalue homomorphism.

theorem HeckeRing.GL2.Eigenform.eigenvalueHom_heckeTCuspNat {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) {p : ℕ} (hp : Nat.Prime p) : (f.eigenvalueHom h₁) ⟨heckeTCuspNat k p, ⋯⟩ = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

On a prime-index Hecke operator, the eigenvalue homomorphism of a normalised full eigenform is its corresponding Fourier coefficient.

theorem HeckeRing.GL2.Eigenform.isIntegral_eigenvalueHom {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (hk : 2 ≤ k) (T : ↥(TauCeti.heckeTCuspPrimeAlgebra N k)) : IsIntegral ℤ ((f.eigenvalueHom h₁) T)

In weight at least two, the eigenvalues of a normalised full eigenform on the prime-index Hecke algebra are algebraic integers.

theorem HeckeRing.GL2.Eigenform.isIntegral_qExpansion_coeff {N : ℕ} [NeZero N] {k : ℤ} (f : Eigenform N k) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1) (hk : 2 ≤ k) (n : ℕ) : IsIntegral ℤ ((PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm))

The Fourier coefficients of a normalised full eigenform of weight at least two are algebraic integers.

theorem HeckeRing.GL2.Newform.isIntegral_qExpansion_coeff {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hk : 2 ≤ k) (n : ℕ) : IsIntegral ℤ ((PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm))

The Fourier coefficients of a newform of weight at least two are algebraic integers.

theorem TauCeti.numberField_CoefficientField {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (hk : 2 ≤ k) : NumberField ↥(CoefficientField f)

The coefficient field of a newform of weight at least two is a number field.