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 ℤ)
:
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' : ∀ (γ : { x // x ∈ Γ }), SlashAction.map ℂ k γ s.toFun = s.toFun
Functions ℍ → ℂ
that are invariant under the SlashAction
.
Instances For
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
.
Instances
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)
:
Copy of a SlashInvariantForm
with a new toFun
equal to the old one.
Useful to fix definitional equalities.
Instances For
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)
:
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)
:
@[simp]
theorem
SlashInvariantForm.add_apply
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
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 : α)
:
@[simp]
theorem
SlashInvariantForm.smul_apply
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
{α : Type u_2}
[SMul α ℂ]
[IsScalarTower α ℂ ℂ]
(f : SlashInvariantForm Γ k)
(n : α)
(z : UpperHalfPlane)
:
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)
:
@[simp]
theorem
SlashInvariantForm.neg_apply
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
(f : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
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)
:
@[simp]
theorem
SlashInvariantForm.sub_apply
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instAddCommGroupSlashInvariantForm
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
:
def
SlashInvariantForm.coeHom
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
:
SlashInvariantForm Γ k →+ UpperHalfPlane → ℂ
Additive coercion from SlashInvariantForm
to ℍ → ℂ
.
Instances For
theorem
SlashInvariantForm.coeHom_injective
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
:
Function.Injective ↑SlashInvariantForm.coeHom
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₂
.
Instances For
@[simp]
theorem
SlashInvariantForm.coe_mul
{k₁ : ℤ}
{k₂ : ℤ}
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
(f : SlashInvariantForm Γ k₁)
(g : SlashInvariantForm Γ k₂)
:
↑(SlashInvariantForm.mul f g) = ↑f * ↑g