Modular forms

This file defines modular forms and proves some basic properties about them. Including constructing the graded ring of modular forms.

We begin by defining modular forms and cusp forms as extension of SlashInvariantForms then we define the space of modular forms, cusp forms and prove that the product of two modular forms is a modular form.

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

These are SlashInvariantForm's that are holomorphic and bounded at infinity.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' : ∀ (γ : ↥Γ), SlashAction.map ℂ k γ self.toFun = self.toFun
• holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
• bdd_at_infty' : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)

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

These are SlashInvariantForms that are holomorphic and zero at infinity.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' : ∀ (γ : ↥Γ), SlashAction.map ℂ k γ self.toFun = self.toFun
• holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑self.toSlashInvariantForm
• zero_at_infty' : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ⇑self.toSlashInvariantForm)

class ModularFormClass (F : Type u_2) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] extends SlashInvariantFormClass : Prop

ModularFormClass F Γ k says that F is a type of bundled functions that extend SlashInvariantFormClass by requiring that the functions be holomorphic and bounded at infinity.

• slash_action_eq : ∀ (f : F) (γ : ↥Γ), SlashAction.map ℂ k γ ⇑f = ⇑f
• holo : ∀ (f : F), MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑f
• bdd_at_infty : ∀ (f : F) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ k A ⇑f)

class CuspFormClass (F : Type u_2) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] extends SlashInvariantFormClass : Prop

CuspFormClass F Γ k says that F is a type of bundled functions that extend SlashInvariantFormClass by requiring that the functions be holomorphic and zero at infinity.

• slash_action_eq : ∀ (f : F) (γ : ↥Γ), SlashAction.map ℂ k γ ⇑f = ⇑f
• holo : ∀ (f : F), MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑f
• zero_at_infty : ∀ (f : F) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ k A ⇑f)

instance ModularForm.funLike (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : FunLike (ModularForm Γ k) UpperHalfPlane ℂ

Equations

• One or more equations did not get rendered due to their size.

instance ModularFormClass.modularForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : ModularFormClass (ModularForm Γ k) Γ k

Equations

• (_ : ModularFormClass (ModularForm Γ k) Γ k) = (_ : ModularFormClass (ModularForm Γ k) Γ k)

instance CuspForm.funLike (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : FunLike (CuspForm Γ k) UpperHalfPlane ℂ

Equations

• One or more equations did not get rendered due to their size.

instance CuspFormClass.cuspForm (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (k : ℤ) : CuspFormClass (CuspForm Γ k) Γ k

Equations

• (_ : CuspFormClass (CuspForm Γ k) Γ k) = (_ : CuspFormClass (CuspForm Γ k) Γ k)

theorem ModularForm.toFun_eq_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : ModularForm Γ k) : f.toFun = ⇑f

@[simp]

theorem ModularForm.toSlashInvariantForm_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : ModularForm Γ k) : ⇑f.toSlashInvariantForm = ⇑f

theorem CuspForm.toFun_eq_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} {f : CuspForm Γ k} : f.toFun = ⇑f

@[simp]

theorem CuspForm.toSlashInvariantForm_coe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : CuspForm Γ k) : ⇑f.toSlashInvariantForm = ⇑f

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

instance ModularForm.add {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Add (ModularForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.coe_zero {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : ⇑0 = 0

@[simp]

theorem ModularForm.zero_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (z : UpperHalfPlane) : 0 z = 0

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.coe_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : ModularForm Γ k) : ⇑(-f) = -⇑f

@[simp]

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

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

Equations

• ModularForm.instSub = { sub := fun (f g : ModularForm Γ k) => f + -g }

@[simp]

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

@[simp]

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

instance ModularForm.instAddCommGroupModularForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : AddCommGroup (ModularForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.coeHom_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : ModularForm Γ k) (a : UpperHalfPlane) : ModularForm.coeHom f a = f a

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

Additive coercion from ModularForm to ℍ → ℂ.

Equations

• One or more equations did not get rendered due to their size.

instance ModularForm.instModuleComplexModularFormInstSemiringComplexToAddCommMonoidInstAddCommGroupModularForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Module ℂ (ModularForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

instance ModularForm.instInhabitedModularForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Inhabited (ModularForm Γ k)

Equations

• ModularForm.instInhabitedModularForm = { default := 0 }

def ModularForm.mul {k_1 : ℤ} {k_2 : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ModularForm Γ (k_1 + k_2)

The modular form of weight k_1 + k_2 given by the product of two modular forms of weights k_1 and k_2.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.mul_coe {k_1 : ℤ} {k_2 : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : ModularForm Γ k_1) (g : ModularForm Γ k_2) : ⇑(ModularForm.mul f g) = ⇑f * ⇑g

@[simp]

theorem ModularForm.const_toFun {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (x : ℂ) : ⇑(ModularForm.const x) = Function.const UpperHalfPlane x

@[simp]

theorem ModularForm.const_toSlashInvariantForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (x : ℂ) : (ModularForm.const x).toSlashInvariantForm = SlashInvariantForm.const x

def ModularForm.const {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (x : ℂ) : ModularForm Γ 0

The constant function with value x : ℂ as a modular form of weight 0 and any level.

Equations

• One or more equations did not get rendered due to their size.

instance ModularForm.instOneModularFormOfNatIntInstOfNat {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : One (ModularForm Γ 0)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.one_coe_eq_one {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : ⇑1 = 1

instance ModularForm.instNatCastModularFormOfNatIntInstOfNat (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : NatCast (ModularForm Γ 0)

Equations

• ModularForm.instNatCastModularFormOfNatIntInstOfNat Γ = { natCast := fun (n : ℕ) => ModularForm.const ↑n }

@[simp]

theorem ModularForm.coe_natCast (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (n : ℕ) : ⇑↑n = ↑n

theorem ModularForm.toSlashInvariantForm_natCast (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (n : ℕ) : (↑n).toSlashInvariantForm = ↑n

instance ModularForm.instIntCastModularFormOfNatIntInstOfNat (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : IntCast (ModularForm Γ 0)

Equations

• ModularForm.instIntCastModularFormOfNatIntInstOfNat Γ = { intCast := fun (z : ℤ) => ModularForm.const ↑z }

@[simp]

theorem ModularForm.coe_intCast (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (z : ℤ) : ⇑↑z = ↑z

theorem ModularForm.toSlashInvariantForm_intCast (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (z : ℤ) : (↑z).toSlashInvariantForm = ↑z

instance CuspForm.hasAdd {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Add (CuspForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CuspForm.coe_zero {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : ⇑0 = 0

@[simp]

theorem CuspForm.zero_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (z : UpperHalfPlane) : 0 z = 0

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CuspForm.coe_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : CuspForm Γ k) : ⇑(-f) = -⇑f

@[simp]

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

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

Equations

• CuspForm.instSub = { sub := fun (f g : CuspForm Γ k) => f + -g }

@[simp]

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

@[simp]

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

instance CuspForm.instAddCommGroupCuspForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : AddCommGroup (CuspForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CuspForm.coeHom_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : CuspForm Γ k) (a : UpperHalfPlane) : CuspForm.coeHom f a = f a

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

Additive coercion from CuspForm to ℍ → ℂ.

Equations

• One or more equations did not get rendered due to their size.

instance CuspForm.instModuleComplexCuspFormInstSemiringComplexToAddCommMonoidInstAddCommGroupCuspForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Module ℂ (CuspForm Γ k)

Equations

• One or more equations did not get rendered due to their size.

instance CuspForm.instInhabitedCuspForm {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Inhabited (CuspForm Γ k)

Equations

• CuspForm.instInhabitedCuspForm = { default := 0 }

instance CuspForm.instModularFormClass {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] : ModularFormClass F Γ k

Equations

• (_ : ModularFormClass F Γ k) = (_ : ModularFormClass F Γ k)

def ModularForm.mcast {a : ℤ} {b : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (h : a = b) (f : ModularForm Γ a) : ModularForm Γ b

Cast for modular forms, which is useful for avoiding Heqs.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularForm.gradedMonoid_eq_of_cast {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {a : GradedMonoid (ModularForm Γ)} {b : GradedMonoid (ModularForm Γ)} (h : a.fst = b.fst) (h2 : ModularForm.mcast h a.snd = b.snd) : a = b

instance ModularForm.instGOneIntModularFormToZeroToCommMonoidWithZeroInstCommSemiringInt (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : GradedMonoid.GOne (ModularForm Γ)

Equations

• ModularForm.instGOneIntModularFormToZeroToCommMonoidWithZeroInstCommSemiringInt Γ = { one := 1 }

instance ModularForm.instGMulIntModularFormInstAddInt (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : GradedMonoid.GMul (ModularForm Γ)

Equations

• ModularForm.instGMulIntModularFormInstAddInt Γ = { mul := fun {i j : ℤ} (f : ModularForm Γ i) (g : ModularForm Γ j) => ModularForm.mul f g }

instance ModularForm.instGCommRing (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : DirectSum.GCommRing (ModularForm Γ)

Equations

• ModularForm.instGCommRing Γ = DirectSum.GCommRing.mk (_ : ∀ (a b : GradedMonoid (ModularForm Γ)), a * b = b * a)

instance ModularForm.instGAlgebra (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : DirectSum.GAlgebra ℂ (ModularForm Γ)

Equations

• One or more equations did not get rendered due to their size.