Restriction and trace preserve the cusp forms

For subgroups Γ' ≤ Γ of GL₂(ℝ) of determinant one, the cusp-form submodule of Mathlib's ModularForm.cuspFormSubmodule is preserved by both maps between M_k(Γ) and M_k(Γ'): restricting a cusp form to Γ' keeps it cuspidal (ModularForm.restrict_mem_cuspFormSubmodule), and so does tracing a cusp form from Γ' up to Γ (ModularForm.traceₗ_mem_cuspFormSubmodule), because the trace of a cusp form is Mathlib's CuspForm.trace.

Main results

• ModularForm.restrict_mem_cuspFormSubmodule: restriction preserves cusp forms.
• ModularForm.traceₗ_mem_cuspFormSubmodule: the trace preserves cusp forms.

theorem ModularForm.restrict_mem_cuspFormSubmodule {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) {f : ModularForm Γ k} (hf : f ∈ cuspFormSubmodule Γ k) : restrict h f ∈ cuspFormSubmodule Γ' k

Restricting a cusp form for Γ to a subgroup Γ' gives a cusp form for Γ'.

theorem ModularForm.traceₗ_mem_cuspFormSubmodule {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] [Γ'.IsFiniteRelIndex Γ] {f : ModularForm Γ' k} (hf : f ∈ cuspFormSubmodule Γ' k) : (traceₗ Γ) f ∈ cuspFormSubmodule Γ k

The trace of a cusp form is a cusp form.