def ModForm_mk (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

Equations

• ModForm_mk Γ k f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

theorem ModForm_mk_inj (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : f ≠ 0) : ModForm_mk Γ k f ≠ 0

def CuspForm_to_ModularForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

Equations

• CuspForm_to_ModularForm Γ k = { toFun := fun (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) => ModForm_mk Γ k f, map_add' := ⋯, map_smul' := ⋯ }

def CuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

Equations

• CuspFormSubmodule Γ k = LinearMap.range (CuspForm_to_ModularForm Γ k)

def CuspForm_iso_CuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k ≃ₗ[ℂ] ↥(CuspFormSubmodule Γ k)

Equations

• CuspForm_iso_CuspFormSubmodule Γ k = LinearEquiv.ofInjective (CuspForm_to_ModularForm Γ k) ⋯

theorem mem_CuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : f ∈ CuspFormSubmodule Γ k) : ∃ (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k), f = (CuspForm_to_ModularForm Γ k) g

@[instance 100]

instance CuspFormSubmodule.funLike {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : FunLike (↥(CuspFormSubmodule Γ k)) UpperHalfPlane ℂ

Equations

• CuspFormSubmodule.funLike = { coe := fun (f : ↥(CuspFormSubmodule Γ k)) => (↑f).toFun, coe_injective' := ⋯ }

instance instCuspFormClassSubtypeModularFormMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLMemSubmoduleComplexCuspFormSubmodule (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspFormClass (↥(CuspFormSubmodule Γ k)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

def IsCuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : Prop

Equations

• IsCuspForm Γ k f = (f ∈ CuspFormSubmodule Γ k)

def IsCuspForm_to_CuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

Equations

• IsCuspForm_to_CuspForm Γ k f hf = ⋯.choose

theorem CuspForm_to_ModularForm_coe (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : (IsCuspForm_to_CuspForm Γ k f hf).toSlashInvariantForm = f.toSlashInvariantForm

theorem CuspForm_to_ModularForm_Fun_coe (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hf : IsCuspForm Γ k f) : (IsCuspForm_to_CuspForm Γ k f hf).toFun = f.toFun

theorem IsCuspForm_iff_coeffZero_eq_zero (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : IsCuspForm (CongruenceSubgroup.Gamma 1) k f ↔ (PowerSeries.coeff 0) (ModularFormClass.qExpansion 1 f) = 0

theorem CuspFormSubmodule_mem_iff_coeffZero_eq_zero (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : f ∈ CuspFormSubmodule (CongruenceSubgroup.Gamma 1) k ↔ (PowerSeries.coeff 0) (ModularFormClass.qExpansion 1 f) = 0