A good Hecke eigenvector in the new part with a₁ = 0 vanishes

The one statement both multiplicity one and strong multiplicity one run on. For a cusp form in S_k(N, χ) that is an eigenvector of the Hecke ring at every prime not dividing N, the eigenvector recurrences propagate a₁ = 0 to the vanishing of every coefficient at an index coprime to N (qExpansion_coeff_eq_zero_of_forall_prime_heckeRingHomCusp_of_one_eq_zero_of_coprime); the Main Lemma (TauCeti.mem_cuspFormsOld_of_forall_coprime_qExpansion_coeff_eq_zero) then puts the form in the old part, and the old and new parts meet only in 0.

Both consumers reach their theorem by producing such an eigenvector, and neither gets one for free: a difference or combination is a Hecke eigenvector only once the two forms are known to share an eigenvalue at each good prime. Multiplicity one assumes that agreement and forms a₁(g) • f - a₁(f) • g; strong multiplicity one first extends agreement from the complement of a finite set to every good index (EigenformAwayFromLevel.eigenvalue_eq_of_forall_notMem) and only then takes the difference of the two newforms.

Main results

• HeckeRing.GL2.mem_cuspFormsOld_of_forall_prime_heckeRingHomCusp_of_one_eq_zero: a good Hecke eigenvector of S_k(N, χ) with a₁ = 0 is old.
• HeckeRing.GL2.eq_zero_of_forall_prime_heckeRingHomCusp_of_one_eq_zero_of_mem_cuspFormsNew: in the new part, it is zero.

References

• T. Miyake, Modular forms, Theorem 4.6.13.

theorem HeckeRing.GL2.mem_cuspFormsOld_of_forall_prime_heckeRingHomCusp_of_one_eq_zero {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {F : ↥(cuspFormCharSpace k χ)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) F = c • F) (h1 : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑F) = 0) : ↑F ∈ TauCeti.cuspFormsOld N k

A good Hecke eigenvector with a₁ = 0 is old: a cusp form in S_k(N, χ) that is an eigenvector of the Hecke ring at every prime not dividing N and has first q-expansion coefficient 0 lies in the old subspace, by the Main Lemma.

theorem HeckeRing.GL2.eq_zero_of_forall_prime_heckeRingHomCusp_of_one_eq_zero_of_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {F : ↥(cuspFormCharSpace k χ)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) F = c • F) (h1 : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑F) = 0) (hnew : ↑F ∈ TauCeti.cuspFormsNew N k) : ↑F = 0

A good Hecke eigenvector in the new part with a₁ = 0 is zero: a cusp form in S_k(N, χ)ᵐᵉʷ that is an eigenvector of the Hecke ring at every prime not dividing N and has first q-expansion coefficient 0 vanishes.