The squarefree decomposition of a form with vanishing coprime coefficients

Miyake's Lemma 4.6.7: a cusp form f ∈ S_k(Γ₁(N), χ) whose q-expansion vanishes at every index coprime to a squarefree l is, coefficient by coefficient, a sum ∑_{q ∈ l.primeFactors} V_q F_q over the primes q dividing l, of level-raises of forms F_q of level N l² / q with nebentypus lowered along N l² / q ∣ N l²: a_n(f) = ∑_{q ∈ l.primeFactors, q ∣ n} a_{n/q}(F_q). The prime peeled at each step is the one of Newforms/Descent/CharacterSpace.lean (exists_mem_cuspFormCharSpace_qExpansion_coeff_eq_ite_dvd_of_qExpansionSupportedOnDvd).

Main results

• TauCeti.exists_qExpansion_coeff_eq_sum_primeFactors_of_squarefree: Lemma 4.6.7, coefficient by coefficient.
• TauCeti.exists_coe_eq_sum_coe_levelRaise_of_squarefree: the same decomposition as an equality of functions rather than of coefficients, which is the form an arbitrary operator consumes. The two differ by q-expansion injectivity at the raised level.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/SquarefreeDecomp.lean, theorem squarefree_decomp_with_lower_level and its Miyake467Decomp_* helpers. The source states the decomposition through a bundled Prop-valued definition and transports forms across equalities of levels; here the conclusion is stated directly and levels are related by divisibility (CuspForm.ofLe).

References

• T. Miyake, Modular forms, Lemma 4.6.7.

theorem TauCeti.exists_qExpansion_coeff_eq_sum_primeFactors_of_squarefree {k : ℤ} {N : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) {l : ℕ} (hsq : Squarefree l) (hvan : ∀ (n : ℕ), n.Coprime l → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : ∃ (F : (q : ℕ) → q ∈ l.primeFactors → CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N * l ^ 2 / q))) k) (χ' : (q : ℕ) → q ∈ l.primeFactors → (ZMod (N * l ^ 2 / q))ˣ →* ℂˣ), (∀ (q : ℕ) (hq : q ∈ l.primeFactors), F q hq ∈ cuspFormCharSpace k (χ' q hq)) ∧ (∀ (q : ℕ) (hq : q ∈ l.primeFactors), (χ' q hq).comp (ZMod.unitsMap ⋯) = χ.comp (ZMod.unitsMap ⋯)) ∧ ∀ (n : ℕ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = ∑ q ∈ l.primeFactors.attach, if ↑q ∣ n then (PowerSeries.coeff (n / ↑q)) (UpperHalfPlane.qExpansion 1 ⇑(F ↑q ⋯)) else 0

Miyake's Lemma 4.6.7: the squarefree decomposition. If f ∈ S_k(Γ₁(N), χ) vanishes at every index coprime to a squarefree l, then a_n(f) = ∑_{q ∈ l.primeFactors, q ∣ n} a_{n/q}(F q), the sum over the primes q dividing l, for forms F q ∈ S_k(Γ₁(N l² / q), χ' q) with χ' q lying over χ: coefficient by coefficient, f = ∑_{q ∈ l.primeFactors} V_q (F q).

theorem TauCeti.exists_coe_eq_sum_coe_levelRaise_of_squarefree {k : ℤ} {M : ℕ} [NeZero M] {l : ℕ} (hsq : Squarefree l) {χ : (ZMod M)ˣ →* ℂˣ} {Δ : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k} (hΔ : Δ ∈ cuspFormCharSpace k χ) (hvan : ∀ (n : ℕ), n.Coprime l → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑Δ) = 0) : ∃ (F : (q : ℕ) → q ∈ l.primeFactors → CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (M * l ^ 2 / q))) k) (χ' : (q : ℕ) → q ∈ l.primeFactors → (ZMod (M * l ^ 2 / q))ˣ →* ℂˣ), (∀ (q : ℕ) (hq : q ∈ l.primeFactors), F q hq ∈ cuspFormCharSpace k (χ' q hq)) ∧ (∀ (q : ℕ) (hq : q ∈ l.primeFactors), (χ' q hq).comp (ZMod.unitsMap ⋯) = χ.comp (ZMod.unitsMap ⋯)) ∧ ⇑Δ = ∑ q ∈ l.primeFactors.attach, ⇑(CuspForm.levelRaise ↑q ⋯ (F ↑q ⋯))

The squarefree decomposition, as an identity of functions. For Δ ∈ S_k(Γ₁(M), χ) with a_n(Δ) = 0 at the indices coprime to a squarefree l, the peeled pieces F_q of level M l² / q (Lemma 4.6.7) satisfy Δ = ∑_{q ∣ l} V_q F_q as functions on ℍ: both sides are cusp forms of level Γ₁(M l²) with the same q-expansion.