The descent of a cusp form to the lower level

For a prime p ∣ N and f ∈ S_k(Γ₁(N), χ) whose nebentypus χ is the pull-back of a character χ₀ modulo N / p, the descent slash sum descendSlash k p N f (Newforms/Descent/Sum.lean) is a cusp form of level Γ₁(N / p), in the space of χ₀: it is Γ₀(N / p)-equivariant with nebentypus χ₀ (descendSlash_slash_mapGL_of_nebentypus_of_prime), holomorphic as a sum of slashes of f, and vanishes at the cusps (Newforms/Descent/Cusps.lean). This is the operator f ↦ ∑_v f ∣[k] descendMatrix p N v of Miyake's Lemma 4.6.14, bundled.

Main definitions

• TauCeti.descendCuspForm: the descent of f as a cusp form of level Γ₁(N / p).

Main results

• TauCeti.coe_descendCuspForm: its underlying function is descendSlash k p N f.
• TauCeti.descendCuspForm_mem_cuspFormCharSpace: it lies in S_k(Γ₁(N / p), χ₀).

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/DescentCharSpace.lean, descendSlashSumCuspForm and descendSlashSumCuspForm_mem_charSpace.

References

• T. Miyake, Modular forms, Lemma 4.6.14.

noncomputable def TauCeti.descendCuspForm {p N : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (hpN : p ∣ N) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N / p))) k

The descent of a cusp form. For p ∣ N prime and f ∈ S_k(Γ₁(N), χ) with χ the pull-back of χ₀ modulo N / p, the descent slash sum of f as a cusp form of level Γ₁(N / p).

Equations

• TauCeti.descendCuspForm k hp hpN hcomp hf = { toFun := TauCeti.descendSlash k p N ⇑f, slash_action_eq' := ⋯, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem TauCeti.coe_descendCuspForm {p N : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (hpN : p ∣ N) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : ⇑(descendCuspForm k hp hpN hcomp hf) = descendSlash k p N ⇑f

The underlying function of the descent is the descent slash sum.

theorem TauCeti.descendCuspForm_mem_cuspFormCharSpace {p N : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (hpN : p ∣ N) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : descendCuspForm k hp hpN hcomp hf ∈ cuspFormCharSpace k χ₀

The descent lowers the level of the nebentypus: the descent of f ∈ S_k(Γ₁(N), χ) lies in S_k(Γ₁(N / p), χ₀).