Cusp form submodule and IsCuspForm predicate

This file defines the inclusion of cusp forms into modular forms as a linear map, the cusp form submodule of modular forms, and the IsCuspForm predicate. It also provides a direct constructor ModularForm.toCuspForm for building cusp forms from modular forms with vanishing constant q-expansion coefficient (for 𝒮ℒ).

Main definitions

• CuspForm.toModularFormₗ: the inclusion CuspForm Γ k →ₗ[ℂ] ModularForm Γ k.
• ModularForm.cuspFormSubmodule: the submodule of ModularForm Γ k consisting of cusp forms.
• ModularForm.IsCuspForm: predicate that a modular form lies in the cusp form submodule.
• ModularForm.toCuspForm: builds a CuspForm 𝒮ℒ k from a ModularForm whose q-expansion has vanishing constant term.

Main results

• CuspForm.toModularFormₗ_injective: the inclusion is injective.
• CuspForm.equivCuspFormSubmodule: CuspForm Γ k ≃ₗ[ℂ] cuspFormSubmodule Γ k.
• ModularForm.isCuspForm_iff_coeffZero_eq_zero: for 𝒮ℒ, IsCuspForm is equivalent to the q-expansion having vanishing constant term.

def CuspForm.toModularFormₗ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] : CuspForm Γ k →ₗ[ℂ] ModularForm Γ k

The inclusion of cusp forms into modular forms, as a ℂ-linear map.

Equations

• CuspForm.toModularFormₗ = { toFun := ModularFormClass.modularForm, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CuspForm.toModularFormₗ_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (f : CuspForm Γ k) (z : UpperHalfPlane) : (toModularFormₗ f) z = f z

theorem CuspForm.toModularFormₗ_eq_coe {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (f : CuspForm Γ k) : toModularFormₗ f = ModularFormClass.modularForm f

theorem CuspForm.toModularFormₗ_injective {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] : Function.Injective ⇑toModularFormₗ

noncomputable def ModularForm.cuspFormSubmodule (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) [Γ.HasDetOne] : Submodule ℂ (ModularForm Γ k)

The submodule of ModularForm Γ k consisting of cusp forms, defined as the range of the inclusion CuspForm.toModularFormₗ.

Equations

• ModularForm.cuspFormSubmodule Γ k = CuspForm.toModularFormₗ.range

def ModularForm.IsCuspForm {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (f : ModularForm Γ k) : Prop

A modular form is a cusp form if it lies in the cusp form submodule.

Equations

• f.IsCuspForm = (f ∈ ModularForm.cuspFormSubmodule Γ k)

@[simp]

theorem ModularForm.mem_cuspFormSubmodule_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] {f : ModularForm Γ k} : f ∈ cuspFormSubmodule Γ k ↔ f.IsCuspForm

noncomputable def ModularForm.CuspForm.equivCuspFormSubmodule (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) [Γ.HasDetOne] : CuspForm Γ k ≃ₗ[ℂ] ↥(cuspFormSubmodule Γ k)

The cusp form submodule is linearly equivalent to the type of cusp forms.

Equations

• ModularForm.CuspForm.equivCuspFormSubmodule Γ k = LinearEquiv.ofInjective CuspForm.toModularFormₗ ⋯

theorem ModularForm.isCuspForm_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (f : ModularForm Γ k) : f.IsCuspForm ↔ ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt (⇑f) k

A modular form is a cusp form if and only if it vanishes at every cusp. This is the general characterization valid for any subgroup.

theorem ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [DiscreteTopology ↥Γ] [Γ.HasDetPlusMinusOne] [Fact (IsCusp OnePoint.infty Γ)] [ModularFormClass F Γ k] (f : F) (h : UpperHalfPlane.valueAtInfty ⇑f = 0) : UpperHalfPlane.IsZeroAtImInfty ⇑f

A modular form with valueAtInfty f = 0 is zero at infinity.

theorem ModularForm.isZeroAt_of_coeffZero_eq_zero {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) {c : OnePoint ℝ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsZeroAt (⇑f) k

An 𝒮ℒ modular form with vanishing q-expansion constant term vanishes at every cusp.

def ModularForm.toCuspForm {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

Build a CuspForm 𝒮ℒ k from a ModularForm 𝒮ℒ k whose q-expansion has vanishing constant term. The resulting cusp form has the same underlying function.

Equations

• f.toCuspForm h = { toSlashInvariantForm := f.toSlashInvariantForm, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.toCuspForm_apply {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) (z : UpperHalfPlane) : (f.toCuspForm h) z = f z

theorem ModularForm.isCuspForm_iff_coeffZero_eq_zero {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : f.IsCuspForm ↔ (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0

For 𝒮ℒ modular forms, IsCuspForm is equivalent to the q-expansion having vanishing constant term.