The Fourier coefficients of a good Hecke eigenform, and of a newform #
For an EigenformAwayFromLevel the coefficients are the eigenvalues scaled by a₁; when
a₁ = 1 they are the eigenvalues themselves, as for a Newform (via Newform.isNorm).
Newforms/RingEigenvalue.lean reads the eigenvalue system λ of an EigenformAwayFromLevel off
the multiplication table of the Γ₀(N) Hecke ring, touching no Fourier coefficient. This file
supplies the missing half: the composite Hecke element reads the coefficient at m n from the
coefficient at m, for m coprime to n
(HeckeSlash/Nebentypus/Composite.lean), so at m = 1 the eigenvector equation becomes
a_n(f) = λ_n · a_1(f) for every good index n,
and for a normalised newform, where a_1 = 1, simply a_n(f) = λ_n. That is the form in which
strong multiplicity one is classically stated — Miyake's Theorem 4.6.12 compares the a_n, not
the λ_n — and the identity that turns the eigenvalue identities of RingEigenvalue.lean
(eigenvalue_mul, eigenvalue_prime_pow_add_two) into the Fourier-coefficient conditions of
Diamond–Shurman's Proposition 5.8.5.
Conversely, the coefficient recurrence at every good prime characterises the existence of an
EigenformAwayFromLevel with a prescribed underlying cusp form. In particular, nonvanishing,
coprime multiplicativity, and the prime-power recurrence imply the good-prime recurrence and
hence produce a bundled good Hecke eigenform. This is the away-from-the-level part of the
coefficient characterisation in Diamond–Shurman, Proposition 5.8.5.
The same holds for full Hecke eigenforms once the nebentypus is extended by zero, χ(p) = 0 for
p ∣ N (Mathlib's MulChar.ofUnitHom): at a prime dividing the level the recurrence degenerates
to a_{pm} = a_p a_m, the coefficient form of U_p f = a_p f. Together with the coefficient
identities Eigenform.qExpansion_coeff_mul and Eigenform.qExpansion_coeff_prime_pow_add_two
this gives Proposition 5.8.5 itself on S_k(N, χ): a cusp form with a₁ = 1 is a full Hecke
eigenform exactly when its coefficients are multiplicative at coprime indices and satisfy the
Hecke recurrence along the powers of every prime.
Main results #
HeckeRing.GL2.EigenformAwayFromLevel.qExpansion_coeff_eq_eigenvalue_mul_coeff_one:a_n(f) = λ_n a_1(f)at a good index.exists_toCuspForm_eq_and_χ_eq_iff_ne_zero_and_forall_prime_qExpansion_coeff_prime_mul: a nonzero cusp form of nebentypusχunderlies a good Hecke eigenform exactly when its coefficients satisfy a scalar Hecke recurrence at every good prime.exists_toCuspForm_eq_and_χ_eq_of_qExpansion_coeff_mul_of_prime_pow_add_two: nonvanishing, coprime multiplicativity, and the prime-power recurrences produce a good Hecke eigenform.HeckeRing.GL2.EigenformAwayFromLevel.qExpansion_coeff_eq_eigenvalue:a_n(f) = λ_nfor a normalised good eigenform (e.g. a newform, viaNewform.isNorm), and with it the two classical coefficient identities at the good indices,HeckeRing.GL2.EigenformAwayFromLevel.qExpansion_coeff_mulandHeckeRing.GL2.EigenformAwayFromLevel.qExpansion_coeff_prime_pow_add_two.Eigenform.exists_toCuspForm_eq_and_χ_eq_iff_ne_zero_and_forall_prime_qExpansion_coeff_prime_mul: a cusp form of nebentypusχunderlies a full Hecke eigenform exactly when it is nonzero and its coefficients satisfy a scalar Hecke recurrence at every prime.Eigenform.exists_toCuspForm_eq_and_χ_eq_of_qExpansion_coeff_mul_of_prime_pow_add_two: nonvanishing, coprime multiplicativity, and the prime-power recurrences at every prime produce a full Hecke eigenform.Eigenform.exists_toCuspForm_eq_and_χ_eq_iff_qExpansion_coeff_mul_and_prime_pow_add_two: Diamond–Shurman's Proposition 5.8.5 onS_k(N, χ).
Provenance #
Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08),
projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean —
eigenvalue_eq_fourierCoeff_one (λ_n = a_n for a normalised eigenform) and
eigenform_coeff_multiplicative_one (the divisor-sum form of the coefficient identities). The
source states them for its IsNormalisedEigenform_one predicate and derives them from the
divisor-sum coefficient formula; here they are statements about EigenformAwayFromLevel and
Newform, read off the eigenvector equation through the coprime-index formula of
HeckeSlash/Nebentypus/Composite.lean and the eigenvalue identities of
Newforms/RingEigenvalue.lean.
References #
- F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.8.5.
- T. Miyake, Modular forms, §4.6.
The coefficients of a good Hecke eigenform are its eigenvalues, scaled by a₁:
a_n(f) = λ_n a_1(f) at every index n coprime to the level. The eigenvector equation at n,
read on the first coefficient: the Hecke element multiplies a_1 by λ_n and reads a_n.
The coefficients of a normalised good eigenform are its eigenvalues: a_n(f) = λ_n at
every index n coprime to the level, when a_1(f) = 1. For a Newform the normalisation is
Newform.isNorm.
Multiplicativity of the coefficients of a normalised good eigenform, at good indices:
a_{mn} = a_m a_n when m and n are coprime to each other and to the level
(Diamond–Shurman Proposition 5.8.5 (3)). This is the image of eigenvalue_mul; newness is not
used.
The prime-power recurrence for a normalised good eigenform, at a good prime:
a_{p^{r+2}} = a_p a_{p^{r+1}} - χ(p) p^{k-1} a_{p^r} (Diamond–Shurman
Proposition 5.8.5 (2)). This is the image of eigenvalue_prime_pow_add_two; newness is not
used.
The coefficient recurrence characterises bundled eigen-ness away from the level. A cusp
form f ∈ S_k(N, χ) underlies an EigenformAwayFromLevel exactly when it is nonzero and, at
every prime p ∤ N, its coefficients satisfy
a_{pm} = c_p a_m - χ(p) p^{k-1} a_{m/p} for some scalar c_p and every m.
The scalar is not required to be named as a_p here: that identification needs the separate
normalisation a₁ = 1.
Diamond–Shurman's coefficient relations produce a good Hecke eigenform. Let
f ∈ S_k(N, χ) be nonzero. If its coefficients are multiplicative at coprime indices and
satisfy the Hecke recurrence along the powers of every good prime, then f underlies an
EigenformAwayFromLevel. (Diamond–Shurman state this for normalised f, a₁ = 1, which
implies f ≠ 0.)
Multiplicativity is needed at all coprime indices, rather than only indices prime to N: to prove
the T_p eigen-relation at a good prime, its coefficient recurrence must also hold at indices
containing prime factors of the level.
The coefficient characterisation of full eigenforms #
The coefficient recurrence at every prime characterises full eigen-ness. A cusp form
f ∈ S_k(N, χ) underlies a full Eigenform exactly when it is nonzero and, at every prime p,
its coefficients satisfy a_{pm} = c_p a_m - χ(p) p^{k-1} a_{m/p} for some scalar c_p and every
m, with the nebentypus extended by zero, so that the last term vanishes for p ∣ N.
The scalar is not required to be named as a_p here: that identification needs the separate
normalisation a₁ = 1.
Diamond–Shurman's coefficient relations at every prime produce a full Hecke eigenform.
Let f ∈ S_k(N, χ) be nonzero. If its coefficients are multiplicative at coprime indices and
satisfy the Hecke recurrence along the powers of every prime, with the nebentypus extended by
zero to the primes dividing the level, then f underlies an Eigenform.
Diamond–Shurman, Proposition 5.8.5, on S_k(N, χ). A cusp form f ∈ S_k(N, χ) with
a₁ = 1 underlies a full Hecke eigenform exactly when its coefficients satisfy
a_{mn} = a_m a_nwhenevermandnare coprime, anda_{p^{r+2}} = a_p a_{p^{r+1}} - χ(p) p^{k-1} a_{p^r}for every primepand everyr, with the nebentypus extended by zero,χ(p) = 0forp ∣ N.