Slash invariant forms

This file defines functions that are invariant under a SlashAction which forms the basis for defining ModularForm and CuspForm. We prove several instances for such spaces, in particular that they form a module.

structure SlashInvariantForm (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) : Type

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ s.toFun = s.toFun

Functions ℍ → ℂ that are invariant under the SlashAction.

class SlashInvariantFormClass (F : Type u_1) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) extends FunLike : Type u_1

• coe : F → UpperHalfPlane → ℂ
• coe_injective' : Function.Injective FunLike.coe
• slash_action_eq : ∀ (f : F) (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ ↑f = ↑f

SlashInvariantFormClass F Γ k asserts F is a type of bundled functions that are invariant under the SlashAction.

instance SlashInvariantFormClass.slashInvariantForm (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) : SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k

instance instCoeFunSlashInvariantFormForAllUpperHalfPlaneComplex {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : CoeFun (SlashInvariantForm Γ k) fun x => UpperHalfPlane → ℂ

@[simp]

theorem SlashInvariantForm.toFun_eq_coe {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {f : SlashInvariantForm Γ k} : f.toFun = ↑f

@[simp]

theorem SlashInvariantForm.coe_mk {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : UpperHalfPlane → ℂ) (hf : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ f = f) : ↑{ toFun := f, slash_action_eq' := hf } = f

theorem SlashInvariantForm.ext {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {f : SlashInvariantForm Γ k} {g : SlashInvariantForm Γ k} (h : ∀ (x : UpperHalfPlane), ↑f x = ↑g x) : f = g

def SlashInvariantForm.copy {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (f' : UpperHalfPlane → ℂ) (h : f' = ↑f) : SlashInvariantForm Γ k

Copy of a SlashInvariantForm with a new toFun equal to the old one. Useful to fix definitional equalities.

instance SlashInvariantForm.SlashInvariantFormClass.coeToFun {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} [SlashInvariantFormClass F Γ k] : CoeFun F fun x => UpperHalfPlane → ℂ

theorem SlashInvariantForm.slash_action_eqn {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} [SlashInvariantFormClass F Γ k] (f : F) (γ : { x // x ∈ Γ }) : SlashAction.map ℂ k γ ↑f = ↑f

theorem SlashInvariantForm.slash_action_eqn' {F : Type u_1} (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [SlashInvariantFormClass F Γ k] (f : F) (γ : { x // x ∈ Γ }) (z : UpperHalfPlane) : ↑f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * ↑f z

instance SlashInvariantForm.instCoeTCSlashInvariantForm {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} [SlashInvariantFormClass F Γ k] : CoeTC F (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.SlashInvariantFormClass.coe_coe {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} [SlashInvariantFormClass F Γ k] (f : F) : ↑{ toFun := ↑f, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ ↑f = ↑f) } = ↑f

instance SlashInvariantForm.instAdd {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Add (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.coe_add {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) : ↑(f + g) = ↑f + ↑g

@[simp]

theorem SlashInvariantForm.add_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) : ↑(f + g) z = ↑f z + ↑g z

instance SlashInvariantForm.instZero {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Zero (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.coe_zero {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : ↑0 = 0

instance SlashInvariantForm.instSMul {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] : SMul α (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.coe_smul {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (f : SlashInvariantForm Γ k) (n : α) : ↑(n • f) = n • ↑f

@[simp]

theorem SlashInvariantForm.smul_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane) : ↑(n • f) z = n • ↑f z

instance SlashInvariantForm.instNeg {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Neg (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.coe_neg {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) : ↑(-f) = -↑f

@[simp]

theorem SlashInvariantForm.neg_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (z : UpperHalfPlane) : ↑(-f) z = -↑f z

instance SlashInvariantForm.instSub {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Sub (SlashInvariantForm Γ k)

@[simp]

theorem SlashInvariantForm.coe_sub {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) : ↑(f - g) = ↑f - ↑g

@[simp]

theorem SlashInvariantForm.sub_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) : ↑(f - g) z = ↑f z - ↑g z

instance SlashInvariantForm.instAddCommGroupSlashInvariantForm {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : AddCommGroup (SlashInvariantForm Γ k)

def SlashInvariantForm.coeHom {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : SlashInvariantForm Γ k →+ UpperHalfPlane → ℂ

Additive coercion from SlashInvariantForm to ℍ → ℂ.

theorem SlashInvariantForm.coeHom_injective {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Function.Injective ↑SlashInvariantForm.coeHom

instance SlashInvariantForm.instModuleComplexSlashInvariantFormInstSemiringComplexToAddCommMonoidInstAddCommGroupSlashInvariantForm {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Module ℂ (SlashInvariantForm Γ k)

instance SlashInvariantForm.instOneSlashInvariantFormOfNatIntInstOfNatInt {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} : One (SlashInvariantForm Γ 0)

@[simp]

theorem SlashInvariantForm.one_coe_eq_one {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} : ↑1 = 1

instance SlashInvariantForm.instInhabitedSlashInvariantForm {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} : Inhabited (SlashInvariantForm Γ k)

def SlashInvariantForm.mul {k₁ : ℤ} {k₂ : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) : SlashInvariantForm Γ (k₁ + k₂)

The slash invariant form of weight k₁ + k₂ given by the product of two modular forms of weights k₁ and k₂.

@[simp]

theorem SlashInvariantForm.coe_mul {k₁ : ℤ} {k₂ : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) : ↑(SlashInvariantForm.mul f g) = ↑f * ↑g