Descending complements of the cusp forms from Γ(N)

Let Γ be a subgroup of SL(2, ℤ) containing Γ(N), and let E be a complement of the cusp forms in M_k(Γ(N)) that is stable under slashing by Γ, such as the span of the Eisenstein series of level Γ(N), which is stable under all of SL(2, ℤ). Then the forms on Γ whose restriction to Γ(N) lies in E form a complement of the cusp forms in M_k(Γ). For Γ = Γ₁(N), if E is stable under Γ₀(N), this complement is stable under the diamond operators, so it also splits each nebentypus space M_k(N, χ) against the image of S_k(N, χ). This is how the cusp–Eisenstein decomposition passes from Γ(N) to congruence subgroups and to prescribed nebentypus, in every weight.

Spanning descends by the trace from Γ(N) to Γ. Restricted back to Γ(N), the trace of a form f is a sum of slashes of f by elements of Γ, so it stays in E; the trace of a cusp form is a cusp form; and the trace of the restriction of a form on Γ is that form times the index. The diamond operators slash by elements of Γ₀(N), so they preserve both the descended complement and the cusp forms, and a diamond-stable complement of the cusp forms splits each nebentypus space (isCompl_comap_subtype_range_cuspToModFormCharSpace).

The declarations live in Mathlib's root ModularForm namespace, beside ModularForm.translateₗ, ModularForm.restrictₗ and ModularForm.traceₗ; the lemmas with an explicit modular-form argument can be used with dot notation, as in f.coe_gammaSlashₗ γ.

Main definitions

• ModularForm.gammaSlashₗ: slashing by γ ∈ SL(2, ℤ) as an endomorphism of M_k(Γ(N)).

Main results

• ModularForm.gammaSlashₗ_one, ModularForm.gammaSlashₗ_mul, ModularForm.gammaSlashₗ_of_mem_Gamma: gammaSlashₗ is a right action of SL(2, ℤ) on which Γ(N) acts trivially.
• ModularForm.restrict_diamondOp_eq_gammaSlashₗ: restricted to Γ(N), a diamond operator is slashing by a representative in Γ₀(N).
• ModularForm.restrict_traceₗ_mem: the trace from Γ(N) to Γ, restricted back to Γ(N), preserves a slash-stable subspace.
• ModularForm.isCompl_comap_restrictₗ_cuspFormSubmodule: a Γ-stable complement of the cusp forms of level Γ(N) descends to a complement of the cusp forms on Γ ⊇ Γ(N).
• ModularForm.diamondOp_mem_comap_restrictₗ: on Γ₁(N), the descended complement is stable under the diamond operators.
• ModularForm.isCompl_comap_restrictₗ_charSpace_range_cuspToModFormCharSpace: the descended complement splits M_k(N, χ) against the image of S_k(N, χ).

References

• F. Diamond and J. Shurman, A first course in modular forms, Sections 4.2, 4.5 and 4.6.

noncomputable def ModularForm.gammaSlashₗ {N : ℕ} {k : ℤ} (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Module.End ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)

Slashing by γ ∈ SL(2, ℤ) as an endomorphism of M_k(Γ(N)), which γ normalizes.

@[simp]

theorem ModularForm.coe_gammaSlashₗ {N : ℕ} {k : ℤ} (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k) : ⇑((gammaSlashₗ γ) f) = SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) ⇑f

The underlying function of gammaSlashₗ γ f is the slash f ∣[k] γ.

@[simp]

theorem ModularForm.gammaSlashₗ_one {N : ℕ} {k : ℤ} : gammaSlashₗ 1 = LinearMap.id

Slashing by the identity is the identity.

theorem ModularForm.gammaSlashₗ_mul {N : ℕ} {k : ℤ} (γ δ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : gammaSlashₗ (γ * δ) = gammaSlashₗ δ ∘ₗ gammaSlashₗ γ

Slashing is a right action: slashing by γ * δ is slashing by γ, then by δ.

theorem ModularForm.gammaSlashₗ_of_mem_Gamma {N : ℕ} {k : ℤ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma N) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k) : (gammaSlashₗ γ) f = f

Elements of Γ(N) act trivially on M_k(Γ(N)).

theorem ModularForm.restrict_diamondOp_eq_gammaSlashₗ {N : ℕ} {k : ℤ} (d : (ZMod N)ˣ) (g : ↥(CongruenceSubgroup.Gamma0 N)) (hg : (CongruenceSubgroup.Gamma0Map N).toHomUnits g = d) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : restrict ⋯ ((TauCeti.diamondOp k d) f) = (gammaSlashₗ ↑g) (restrict ⋯ f)

Restricted to Γ(N), the diamond operator ⟨d⟩ on M_k(Γ₁(N)) is slashing by any representative g ∈ Γ₀(N) of d.

theorem ModularForm.restrict_traceₗ_mem {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {S : Type u_1} [SetLike S (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)] [AddSubmonoidClass S (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)] {E : S} (hE : ∀ γ ∈ Γ, ∀ f ∈ E, (gammaSlashₗ γ) f ∈ E) (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k} (hf : f ∈ E) : restrict ⋯ ((traceₗ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ)) f) ∈ E

Restricted back to Γ(N), the trace from Γ(N) to a larger subgroup Γ of SL(2, ℤ) maps an additive submonoid stable under slashing by Γ, such as a subspace, into itself: it is a sum of slashes by elements of Γ.

theorem ModularForm.isCompl_comap_restrictₗ_cuspFormSubmodule {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {E : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)} (hE : IsCompl E (cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)) (hslash : ∀ γ ∈ Γ, ∀ f ∈ E, (gammaSlashₗ γ) f ∈ E) (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) : IsCompl (Submodule.comap (restrictₗ k ℂ ⋯) E) (cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

Descent of a complement of the cusp forms. Let Γ ⊇ Γ(N) be a subgroup of SL(2, ℤ). If E is a complement of the cusp forms in M_k(Γ(N)) stable under slashing by Γ, then the forms on Γ whose restriction to Γ(N) lies in E form a complement of the cusp forms in M_k(Γ).

theorem ModularForm.diamondOp_mem_comap_restrictₗ {N : ℕ} {k : ℤ} {E : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)} (hslash : ∀ γ ∈ CongruenceSubgroup.Gamma0 N, ∀ f ∈ E, (gammaSlashₗ γ) f ∈ E) (d : (ZMod N)ˣ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ Submodule.comap (restrictₗ k ℂ ⋯) E) : (TauCeti.diamondOp k d) f ∈ Submodule.comap (restrictₗ k ℂ ⋯) E

On Γ₁(N), the diamond operators preserve the forms whose restriction to Γ(N) lies in a subspace stable under slashing by Γ₀(N).

theorem ModularForm.isCompl_comap_restrictₗ_charSpace_range_cuspToModFormCharSpace {N : ℕ} {k : ℤ} [NeZero N] {E : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)} (hE : IsCompl E (cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k)) (hslash : ∀ γ ∈ CongruenceSubgroup.Gamma0 N, ∀ f ∈ E, (gammaSlashₗ γ) f ∈ E) (χ : (ZMod N)ˣ →* ℂˣ) : IsCompl (Submodule.comap (TauCeti.modFormCharSpace k χ).subtype (Submodule.comap (restrictₗ k ℂ ⋯) E)) (TauCeti.cuspToModFormCharSpace k χ).range

Descent to a nebentypus. If E is a complement of the cusp forms in M_k(Γ(N)) stable under slashing by Γ₀(N), then the forms of nebentypus χ whose restriction to Γ(N) lies in E form a complement of the image of S_k(N, χ) in M_k(N, χ).