Level-raised newforms span the cusp forms

Every cusp form of level Γ₁(N) is a linear combination of forms V_d g, (V_d g)(τ) = g(dτ), with g a newform of some level M and d * M ∣ N. This is the spanning half of Diamond–Shurman's Theorem 5.8.3, the decomposition

S_k(Γ₁(N)) = ⊕_{M ∣ N} ⊕_{f newform of level M} ⊕_{d ∣ N/M} ℂ · f(dτ).

The eigenvalue-refined spanning theorem says that a cusp form of level Γ₁(N) that is an eigenvector of every Tₚ with p ∤ N is a combination of those V_d g whose newform g has the same eigenvalues at these primes. In particular a good Hecke eigenform of level N shares its eigenvalues at the primes not dividing N with a newform of some level M ∣ N. This is the eigenvalue half of the existence of the newform associated with an eigenform (Diamond–Shurman, Proposition 5.8.4; Miyake, Corollary 4.6.20). Uniqueness of that newform, and hence the statement that the eigenform lies in the span of the V_d g for a single g, needs strong multiplicity one across levels and is not proved here.

Inside the nebentypus space of a newform f of level N the spanning theorem does close up: a good Hecke eigenvector F ∈ S_k(N, χ_f) with the eigenvalues of f is the multiple a₁(F) • f of f (Newform.eq_qExpansion_coeff_one_smul_of_forall_prime_heckeTCuspNat_eq_smul, the whole-space form of Diamond–Shurman's Theorem 5.8.2). The level-raised newforms spanning F with compatible nebentypus have level N by the divisor-level rigidity Newform.level_eq_of_dvd_of_forall_prime_eigenvalue_eq, hence are f by strong multiplicity one, and the others lie in nebentypus spaces meeting S_k(N, χ_f) only in 0.

Main results

• HeckeRing.GL2.Newform.span_levelRaise_eq_top: the level-raised newforms span S_k(Γ₁(N)).
• HeckeRing.GL2.Newform.mem_span_levelRaise_of_forall_heckeTCuspNat_eq_smul: a simultaneous eigenvector of the good Tₚ lies in the span of the level-raised newforms with its eigenvalues.
• HeckeRing.GL2.Newform.exists_newform_eigenvalue_eq_of_forall_heckeTCuspNat_eq_smul and HeckeRing.GL2.EigenformAwayFromLevel.exists_newform_eigenvalue_eq: a nonzero simultaneous eigenvector of the good Tₚ, in particular a good Hecke eigenform, shares its eigenvalues at the primes not dividing the level with a newform of divisor level.
• HeckeRing.GL2.Newform.eq_qExpansion_coeff_one_smul_of_forall_prime_heckeTCuspNat_eq_smul: a good Hecke eigenvector of S_k(N, χ) with the eigenvalues of a newform f of level N and nebentypus χ is the multiple a₁ • f of f.

Provenance

The last statement is that of strongMultiplicityOne_constMul in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bd), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/ConstantMultiple.lean: a newform and a good Hecke eigenform sharing eigenvalues are proportional. It is proved here independently, from the spanning theorem, the divisor-level rigidity of the level and the independence of the nebentypus spaces.

References

• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2, Theorem 5.8.3 and Proposition 5.8.4.
• T. Miyake, Modular forms, Theorem 4.6.13 and Corollary 4.6.20.

theorem HeckeRing.GL2.Newform.span_levelRaise_eq_top (N : ℕ) [NeZero N] (k : ℤ) : Submodule.span ℂ {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k | ∃ (M : ℕ) (d : ℕ) (x : NeZero M) (x_1 : NeZero d) (h : d * M ∣ N) (g : Newform M k), TauCeti.CuspForm.levelRaise d ⋯ g.toCuspForm = F} = ⊤

The level-raised newforms span S_k(Γ₁(N)) (Diamond–Shurman, Theorem 5.8.3, spanning): every cusp form of level Γ₁(N) is a combination of forms V_d g, (V_d g)(τ) = g(dτ), with g a newform of some level M and d * M ∣ N. The NeZero binders only make the instances available; they follow from d * M ∣ N.

theorem HeckeRing.GL2.Newform.mem_span_levelRaise_of_forall_heckeTCuspNat_eq_smul {N : ℕ} {k : ℤ} [NeZero N] {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} {a : (p : ℕ) → Nat.Prime p → p.Coprime N → ℂ} (hF : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), (heckeTCuspNat k p) F = a p hp hpN • F) : F ∈ Submodule.span ℂ {G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k | ∃ (M : ℕ) (d : ℕ) (x : NeZero M) (x_1 : NeZero d) (h : d * M ∣ N) (g : Newform M k), (∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), g.eigenvalue ⟨p, ⋯⟩ ⋯ = a p hp hpN) ∧ TauCeti.CuspForm.levelRaise d ⋯ g.toCuspForm = G}

A simultaneous eigenvector of the good Hecke operators lies in the span of the level-raised newforms with its eigenvalues. If a cusp form F of level Γ₁(N) satisfies Tₚ F = aₚ F at every prime p ∤ N, then F is a combination of forms V_d g, d * M ∣ N, with g a newform of level M whose eigenvalue at every prime p ∤ N is aₚ.

theorem HeckeRing.GL2.Newform.exists_newform_eigenvalue_eq_of_forall_heckeTCuspNat_eq_smul {N : ℕ} {k : ℤ} [NeZero N] {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hF0 : F ≠ 0) {a : (p : ℕ) → Nat.Prime p → p.Coprime N → ℂ} (hF : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), (heckeTCuspNat k p) F = a p hp hpN • F) : ∃ (M : ℕ) (x : NeZero M) (hM : M ∣ N) (g : Newform M k), ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), g.eigenvalue ⟨p, ⋯⟩ ⋯ = a p hp hpN

A nonzero simultaneous eigenvector of the good Hecke operators has the eigenvalues of a newform of divisor level. If a nonzero cusp form F of level Γ₁(N) satisfies Tₚ F = aₚ F at every prime p ∤ N, then some newform g of some level M ∣ N has eigenvalue aₚ at every prime p ∤ N.

theorem HeckeRing.GL2.EigenformAwayFromLevel.exists_newform_eigenvalue_eq {N : ℕ} {k : ℤ} [NeZero N] (f : EigenformAwayFromLevel N k) : ∃ (M : ℕ) (x : NeZero M) (hM : M ∣ N) (g : Newform M k), ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), g.eigenvalue ⟨p, ⋯⟩ ⋯ = f.eigenvalue ⟨p, ⋯⟩ hpN

A good Hecke eigenform has the eigenvalues of a newform of divisor level: for a good Hecke eigenform f of level N there are a divisor M of N and a newform g of level M whose eigenvalue at every prime p ∤ N equals that of f. This is the eigenvalue half of the existence of the newform associated with f (Diamond–Shurman, Proposition 5.8.4; Miyake, Corollary 4.6.20); the uniqueness of g is a separate statement.

The good eigensystem of a newform spans a line in its nebentypus space

theorem HeckeRing.GL2.Newform.eq_qExpansion_coeff_one_smul_of_forall_prime_heckeTCuspNat_eq_smul {N : ℕ} {k : ℤ} [NeZero N] (f : Newform N k) {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hF : F ∈ cuspFormCharSpace k f.χ) (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), (heckeTCuspNat k p) F = f.eigenvalue ⟨p, ⋯⟩ hpN • F) : F = (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑F) • f.toCuspForm

A good Hecke eigenvector of S_k(N, χ) with the eigenvalues of a newform f is the multiple a₁(F) • f of f (Diamond–Shurman, Theorem 5.8.2, on the whole nebentypus space rather than its new part): if F ∈ S_k(N, χ_f) satisfies Tₚ F = λₚ(f) • F at every prime p ∤ N, then F = a₁(F) • f. So the simultaneous eigenspace of the good Tₚ in S_k(N, χ_f) for the eigensystem of f is the line spanned by f.