The descent commutes with the level-raise

Miyake's Lemma 4.6.6 (2): for a prime p ∣ N and l coprime to p, the descent slash sum at level l N of the level-raise V_l f of f ∈ S_k(Γ₁(N), χ) is the level-raise of the descent slash sum of f at level N, provided χ is the pull-back of a character modulo N / p. The upper-triangular members !![1, b; 0, p] of the two families are matched by the permutation b ↦ l b mod p of the residues, and the extra members (present when p² ∤ N) by conjugating the level-l N one back to level N, where the nebentypus shows the two candidates give the same slash.

The identity is what lets the descent be computed piece by piece on the squarefree decomposition (Newforms/SquarefreeDecomposition.lean): the pieces are level-raises V_q F_q, and the descent of each is V_q of the descent of F_q, a form supported on the multiples of q. That is how the coefficient formula of the descent, the core of Miyake's Lemma 4.6.14, is proved.

Main results

• TauCeti.descendSlash_coe_levelRaise_mul_left_of_comp_of_mem_modFormCharSpace, and its cusp-form case TauCeti.descendSlash_coe_levelRaise_mul_left_of_comp_of_mem_cuspFormCharSpace: descendSlash k p (l N) (V_l f) = l ^ (1 - k) • (descendSlash k p N f ∣[k] diag(l, 1)), that is, V_l of the descent.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/LevelCommute.lean (level_commute_delta and its delta_* helpers, descendCosetList_slash_sum_rep_invariance, extra_rep_levelRaise_bridge). The source's modularFormLevelRaise is this repository's ModularForm.levelRaise, its levelRaiseConjOfDvd is conjScale, and its explicit coset list is the family descendMatrix; the statements are re-proved on those. The source's level_commute_delta also assumes l ∣ N / p, which the argument does not use, so it is dropped here.

References

• T. Miyake, Modular forms, Lemma 4.6.6.

theorem TauCeti.descendSlash_coe_levelRaise_mul_left_of_comp_of_mem_modFormCharSpace {p l : ℕ} (k : ℤ) {N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpl : p.Coprime l) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) : descendSlash k p (l * N) ⇑(ModularForm.levelRaise l ⋯ f) = ↑l ^ (1 - k) • SlashAction.map k (scaleGL l) (descendSlash k p N ⇑f)

The descent commutes with the level-raise (Miyake, Lemma 4.6.6 (2)). For a prime p ∣ N, l coprime to p, and f ∈ M_k(Γ₁(N), χ) with χ the pull-back of a character modulo N / p, the descent slash sum at level l N of V_l f is V_l of the descent slash sum of f at level N: descendSlash k p (l N) (V_l f) = l ^ (1 - k) • (descendSlash k p N f ∣[k] diag(l, 1)).

theorem TauCeti.descendSlash_coe_levelRaise_mul_left_of_comp_of_mem_cuspFormCharSpace {p l : ℕ} (k : ℤ) {N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpl : p.Coprime l) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : descendSlash k p (l * N) ⇑(CuspForm.levelRaise l ⋯ f) = ↑l ^ (1 - k) • SlashAction.map k (scaleGL l) (descendSlash k p N ⇑f)

The descent commutes with the level-raise, on cusp forms. For a prime p ∣ N, l coprime to p, and f ∈ S_k(Γ₁(N), χ) with χ the pull-back of a character modulo N / p, descendSlash k p (l N) (V_l f) = l ^ (1 - k) • (descendSlash k p N f ∣[k] diag(l, 1)).