The descent of a level-raise

For a prime p ∣ N and g slash-invariant of level Γ₁(N / p), every member of the descent family descendMatrix p N slashes the level-raise V_p g = p^(1-k) • (g ∣[k] scaleGL p) (a form of level Γ₁(N)) back to p⁻¹ • g: the upper-triangular members !![1, b; 0, p] because (V_p g) ((τ + b) / p) = g (τ + b) = g τ (smul_slash_scaleGL_slash_upperTriRep), and the extra member because its Γ₀(N / p) factor lies in Γ(N / p). So the descent slash sum of V_p g is the scalar multiple (|family| / p) • g, with |family| = p when p² ∣ N and p + 1 otherwise. This is the computation behind the coefficient formula of the descent in Miyake's proof of Lemma 4.6.14.

Main results

• TauCeti.smul_slash_scaleGL_slash_descendMatrix: every member of the family slashes V_p g = p^(1-k) • (g ∣[k] scaleGL p) to p⁻¹ • g, for g slash-invariant of level Γ₁(N / p).
• TauCeti.descendSlash_smul_slash_scaleGL: hence descendSlash k p N (p^(1-k) • (g ∣[k] scaleGL p)) = (|family| / p) • g.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/HeckeDescent.lean (V_p_slash_descendCoset) and StrongMultiplicityOne/DescentCharSpace.lean (slash_sum_V_p_pointwise_eq_smul_g_low). The source's modularFormLevelRaise is this repository's ModularForm.levelRaise, and its descendCosetList the family descendMatrix; the statements are re-proved on those.

References

• T. Miyake, Modular forms, Lemma 4.6.14.

theorem TauCeti.smul_slash_scaleGL_slash_descendMatrix {p N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N / p))) k] (g : F) (v : Fin (descendMatrixCount p N)) : SlashAction.map k (descendMatrix p N v) (↑p ^ (1 - k) • SlashAction.map k (scaleGL p) ⇑g) = (↑p)⁻¹ • ⇑g

Every member of the descent family slashes a level-raise back to the form. For p ∣ N prime and g slash-invariant of level Γ₁(N / p), with V_p g = p^(1-k) • (g ∣[k] scaleGL p), (V_p g) ∣[k] descendMatrix p N v = p⁻¹ • g for every v.

theorem TauCeti.descendSlash_smul_slash_scaleGL {p N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N / p))) k] (g : F) : descendSlash k p N (↑p ^ (1 - k) • SlashAction.map k (scaleGL p) ⇑g) = (↑(descendMatrixCount p N) / ↑p) • ⇑g

The descent of a level-raise is a multiple of the form. For p ∣ N prime and g slash-invariant of level Γ₁(N / p), with V_p g = p^(1-k) • (g ∣[k] scaleGL p), descendSlash k p N (V_p g) = (|family| / p) • g. This is the coefficient formula of the descent on a level-raise, the input to Miyake's Lemma 4.6.14.