Newforms are full Hecke eigenforms

A newform is, by definition, a normalised good Hecke eigenform in the new subspace (Miyake's primitive form): eigen-ness is demanded only at the indices coprime to the level. This file proves that it is an eigenvector of T_n at every positive index, including the primes dividing the level, with eigenvalue the Fourier coefficient a_n (Diamond–Shurman, Theorem 5.8.2; Miyake, Theorem 4.6.13; the bad-prime eigenvalues go back to Atkin–Lehner and Li). This is the bridge between the two definitions of "newform" in the literature: Diamond–Shurman define a newform as a normalised full eigenform in the new subspace, and their Theorem 5.8.2 is exactly the statement that Miyake's primitive forms are such.

The textbook route passes through the stability of the new subspace under the bad-prime operators U_p. The route here needs no bad-prime stability: for p ∣ N the operator U_p = T_p commutes with the good T_q in the commutative Γ₀(N) Hecke ring, so U_p f is a good eigenvector of S_k(N, χ) with the eigenvalues of f, hence the multiple a₁(U_p f) • f of f (Newform.eq_qExpansion_coeff_one_smul_of_forall_prime_heckeTCuspNat_eq_smul), and a₁(U_p f) = a_p(f).

Main definitions

• HeckeRing.GL2.Newform.toEigenform: a newform as a full Hecke eigenform.

Main results

• HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smul: U_p f = a_p(f) • f for a newform f and a prime p ∣ N, the bad-prime eigenvector equation.
• HeckeRing.GL2.Newform.heckeTCuspNat_eq_qExpansion_coeff_smul: T_p f = a_p(f) • f at every prime p, the primes dividing the level (where T_p = U_p) included.
• HeckeRing.GL2.Newform.toEigenform_eigenvalue_eq_qExpansion_coeff: the eigenvalue of a newform at every positive index is its Fourier coefficient there.

Provenance

The same theorem is proved in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Newforms/FullEigenform.lean: Newform.heckeT_n_cusp_bad_prime_eq there is the bad-prime equation U_p f = a_p(f) • f, and Newform.isFullEigenform there is Newform.toEigenform here, stated as a predicate on the cusp form rather than as a bundled Eigenform. The proofs are independent: the source takes the textbook route through the stability of the new subspace under the bad-prime U_p (heckeT_n_cusp_preserves_cuspFormsNewExtended_bad, via the Petersson adjoint of U_p), which this file does not use.

References

• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2.
• T. Miyake, Modular forms, Theorem 4.6.13.
• A. O. L. Atkin and J. Lehner, Hecke operators on Γ₀(m), Math. Ann. 185 (1970), 134–160.
• W.-C. W. Li, Newforms and functional equations, Math. Ann. 212 (1975), 285–315.

The bad-prime eigenvalues

theorem HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smul {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) : (heckeUCuspNat k p hp hpN) f.toCuspForm = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) • f.toCuspForm

A newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) (Atkin–Lehner; Li; Diamond–Shurman, Theorem 5.8.2; Miyake, Theorem 4.6.13). Together with the good eigensystem this makes a newform a full Hecke eigenform (Newform.toEigenform). The statement is on the bad-prime operator heckeUCuspNat, matching the U_p-spelled API of HeckeSlash/BadPrime; Newform.heckeTCuspNat_eq_qExpansion_coeff_smul is the statement at every prime.

The full eigenform

noncomputable def HeckeRing.GL2.Newform.toEigenform {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : Eigenform N k

A newform is a full Hecke eigenform (Diamond–Shurman, Theorem 5.8.2; Miyake, Theorem 4.6.13): its good eigensystem, together with the bad-prime eigenvector equations U_p f = a_p(f) • f, makes it an eigenvector of T_n at every positive index. This is the bridge between Miyake's primitive form, the definition of Newform here, and Diamond–Shurman's newform, defined as a normalised full eigenform in the new subspace.

Equations

• f.toEigenform = f.toEigenform ⋯

@[simp]

theorem HeckeRing.GL2.Newform.toEigenform_toCuspForm {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : f.toEigenform.toCuspForm = f.toCuspForm

@[simp]

theorem HeckeRing.GL2.Newform.toEigenform_χ {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : f.toEigenform.χ = f.χ

theorem HeckeRing.GL2.Newform.toEigenform_qExpansion_coeff_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toEigenform.toCuspForm) = 1

The full eigenform attached to a newform remains normalised.

@[simp]

theorem HeckeRing.GL2.Newform.toEigenform_toEigenformAwayFromLevel {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : f.toEigenform.toEigenformAwayFromLevel = f.toEigenformAwayFromLevel

@[simp]

theorem HeckeRing.GL2.Newform.toEigenform_eigenvalue_eq_qExpansion_coeff {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (n : ℕ+) : f.toEigenform.eigenvalue n = (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

The Hecke eigenvalues of a newform are its Fourier coefficients, at every positive index: T_n f = a_n(f) • f for all n ≥ 1, the primes dividing the level included.

theorem HeckeRing.GL2.Newform.heckeTCuspNat_eq_qExpansion_coeff_smul {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) : (heckeTCuspNat k p) f.toCuspForm = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) • f.toCuspForm

Tₚ f = aₚ(f) • f at every prime p, whether or not p divides the level: the good eigensystem of f and the bad-prime equation Newform.heckeUCuspNat_eq_qExpansion_coeff_smul (at a prime p ∣ N the operator is U_p, heckeUCuspNat_eq_heckeTCuspNat) in one statement.