The coefficient characterization of normalized modular eigenforms

A modular form of nebentypus χ with first Fourier coefficient 1 is an eigenform for every positive-index Hecke operator if and only if its coefficients are multiplicative at coprime indices and satisfy the prime-power Hecke recurrence. This includes noncuspidal forms and bad primes: the character in the recurrence is Mathlib's zero-extension MulChar.ofUnitHom χ.

Only positive coefficients are used in the converse. Their uniqueness at nonzero weight recovers the constant-term equation, rather than adding it as an extra hypothesis. Normalization already excludes weight zero and the zero form. The eigenvalues are the Fourier coefficients, so the statement needs neither a bundled eigenvalue function nor choices of scalars.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, Proposition 5.8.5.

theorem TauCeti.forall_heckeTCompositeGamma0_eq_coeff_smul_iff {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (F : ↥(modFormCharSpace k χ)) (h₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑F) = 1) : (∀ (n : ℕ), n ≠ 0 → ((HeckeRing.GL2.heckeRingHomCharSpace k χ) (HeckeRing.GL2.heckeTCompositeGamma0 N n)) F = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑↑F) • F) ↔ (∀ (u v : ℕ), u.Coprime v → (PowerSeries.coeff (u * v)) (UpperHalfPlane.qExpansion 1 ⇑↑F) = (PowerSeries.coeff u) (UpperHalfPlane.qExpansion 1 ⇑↑F) * (PowerSeries.coeff v) (UpperHalfPlane.qExpansion 1 ⇑↑F)) ∧ ∀ (p : ℕ), Nat.Prime p → ∀ (r : ℕ), (PowerSeries.coeff (p ^ (r + 2))) (UpperHalfPlane.qExpansion 1 ⇑↑F) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑↑F) * (PowerSeries.coeff (p ^ (r + 1))) (UpperHalfPlane.qExpansion 1 ⇑↑F) - (MulChar.ofUnitHom χ) ↑p * ↑p ^ (k - 1) * (PowerSeries.coeff (p ^ r)) (UpperHalfPlane.qExpansion 1 ⇑↑F)

Diamond–Shurman, Proposition 5.8.5, on M_k(N, χ). A modular form with a₁ = 1 is an eigenform for all positive-index Hecke operators exactly when its Fourier coefficients are multiplicative at coprime indices and satisfy the Hecke recurrence at every prime. The character is extended by zero at the bad primes; no constant-term condition or cuspidality is assumed.