Descent of a supported form within a character space

A cusp form G ∈ S_k(Γ₁(M), χ₀ ∘ π) whose q-expansion is supported on the multiples of a divisor p ∣ M, with χ₀ a character modulo M / p, is the level-raise V_p of a period-one function (Newforms/Descent/Basic.lean), and the level-lowering dichotomy (ConductorDichotomy.lean) either finds that function as a cusp form F ∈ S_k(Γ₁(M / p), χ₀), or forces G = 0, when F = 0 will do. Either way a_n(G) = a_{n/p}(F) for p ∣ n and a_n(G) = 0 otherwise: G is V_p F on coefficients. This is the step that lowers the level of one prime at a time in Miyake's proofs of Lemmas 4.6.7 and 4.6.8.

Main results

• TauCeti.exists_mem_cuspFormCharSpace_qExpansion_coeff_eq_ite_dvd_of_qExpansionSupportedOnDvd: peeling a divisor off a form supported on its multiples.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/SquarefreeDecomp.lean: the dichotomy step inside miyake_V_p_descend_identity_with_char, separated out with the lowered character explicit.

References

• T. Miyake, Modular forms, Theorem 4.6.4 and Lemma 4.6.7.

theorem TauCeti.exists_mem_cuspFormCharSpace_qExpansion_coeff_eq_ite_dvd_of_qExpansionSupportedOnDvd {k : ℤ} {M p : ℕ} [NeZero M] (hpM : p ∣ M) (χ₀ : (ZMod (M / p))ˣ →* ℂˣ) {G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k} (hG : G ∈ cuspFormCharSpace k (χ₀.comp (ZMod.unitsMap ⋯))) (hsupp : QExpansionSupportedOnDvd p G) : ∃ F ∈ cuspFormCharSpace k χ₀, ∀ (n : ℕ), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑G) = if p ∣ n then (PowerSeries.coeff (n / p)) (UpperHalfPlane.qExpansion 1 ⇑F) else 0

Peeling a divisor off a form supported on its multiples. If G ∈ S_k(Γ₁(M), χ₀ ∘ π) is supported on the multiples of p ∣ M, where χ₀ is a character modulo M / p, then there is F ∈ S_k(Γ₁(M / p), χ₀) with a_n(G) = a_{n/p}(F) for p ∣ n and a_n(G) = 0 otherwise: G is V_p F on coefficients.