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 ℤ)
:
Functions ℍ → ℂ
that are invariant under the SlashAction
.
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' : ∀ (γ : ↥Γ), SlashAction.map ℂ k γ self.toFun = self.toFun
Instances For
theorem
SlashInvariantForm.slash_action_eq'
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
(self : SlashInvariantForm Γ k)
(γ : ↥Γ)
:
SlashAction.map ℂ k γ self.toFun = self.toFun
class
SlashInvariantFormClass
(F : Type u_1)
(Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)))
(k : outParam ℤ)
[FunLike F UpperHalfPlane ℂ]
:
SlashInvariantFormClass F Γ k
asserts F
is a type of bundled functions that are invariant
under the SlashAction
.
- slash_action_eq : ∀ (f : F) (γ : ↥Γ), SlashAction.map ℂ k γ ⇑f = ⇑f
Instances
theorem
SlashInvariantFormClass.slash_action_eq
{F : Type u_1}
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
[FunLike F UpperHalfPlane ℂ]
[self : SlashInvariantFormClass F Γ k]
(f : F)
(γ : ↥Γ)
:
SlashAction.map ℂ k γ ⇑f = ⇑f
@[instance 100]
instance
SlashInvariantForm.funLike
(Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)))
(k : outParam ℤ)
:
Equations
- SlashInvariantForm.funLike Γ k = { coe := SlashInvariantForm.toFun, coe_injective' := ⋯ }
@[instance 100]
instance
SlashInvariantFormClass.slashInvariantForm
(Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)))
(k : outParam ℤ)
:
SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k
Equations
- ⋯ = ⋯
@[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 : ∀ (γ : ↥Γ), SlashAction.map ℂ k γ f = f)
:
⇑{ toFun := f, slash_action_eq' := hf } = f
theorem
SlashInvariantForm.ext_iff
{Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))}
{k : outParam ℤ}
{f : SlashInvariantForm Γ k}
{g : SlashInvariantForm Γ k}
:
f = g ↔ ∀ (x : UpperHalfPlane), f x = g x
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.
Equations
- f.copy f' h = { toFun := f', slash_action_eq' := ⋯ }
Instances For
theorem
SlashInvariantForm.slash_action_eqn
{F : Type u_1}
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
[FunLike F UpperHalfPlane ℂ]
[SlashInvariantFormClass F Γ k]
(f : F)
(γ : ↥Γ)
:
SlashAction.map ℂ k γ ⇑f = ⇑f
theorem
SlashInvariantForm.slash_action_eqn'
{F : Type u_1}
[FunLike F UpperHalfPlane ℂ]
(k : ℤ)
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))
[SlashInvariantFormClass F Γ k]
(f : F)
(γ : ↥Γ)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instCoeTCOfSlashInvariantFormClass
{F : Type u_1}
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
[FunLike F UpperHalfPlane ℂ]
[SlashInvariantFormClass F Γ k]
:
CoeTC F (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instCoeTCOfSlashInvariantFormClass = { coe := fun (f : F) => { toFun := ⇑f, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.SlashInvariantFormClass.coe_coe
{F : Type u_1}
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
[FunLike F UpperHalfPlane ℂ]
[SlashInvariantFormClass F Γ k]
(f : F)
:
⇑{ toFun := ⇑f, slash_action_eq' := ⋯ } = ⇑f
instance
SlashInvariantForm.instAdd
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Add (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instAdd = { add := fun (f g : SlashInvariantForm Γ k) => { toFun := ⇑f + ⇑g, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.coe_add
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
:
@[simp]
theorem
SlashInvariantForm.add_apply
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instZero
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Zero (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instZero = { zero := { toFun := 0, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.coe_zero
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
⇑0 = 0
instance
SlashInvariantForm.instSMul
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
{α : Type u_2}
[SMul α ℂ]
[IsScalarTower α ℂ ℂ]
:
SMul α (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instSMul = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c • ⇑f, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.coe_smul
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
{α : Type u_2}
[SMul α ℂ]
[IsScalarTower α ℂ ℂ]
(f : SlashInvariantForm Γ k)
(n : α)
:
@[simp]
theorem
SlashInvariantForm.smul_apply
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
{α : Type u_2}
[SMul α ℂ]
[IsScalarTower α ℂ ℂ]
(f : SlashInvariantForm Γ k)
(n : α)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instNeg
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Neg (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instNeg = { neg := fun (f : SlashInvariantForm Γ k) => { toFun := -⇑f, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.coe_neg
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
:
@[simp]
theorem
SlashInvariantForm.neg_apply
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instSub
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Sub (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instSub = { sub := fun (f g : SlashInvariantForm Γ k) => f + -g }
@[simp]
theorem
SlashInvariantForm.coe_sub
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
:
@[simp]
theorem
SlashInvariantForm.sub_apply
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
(f : SlashInvariantForm Γ k)
(g : SlashInvariantForm Γ k)
(z : UpperHalfPlane)
:
instance
SlashInvariantForm.instAddCommGroup
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Equations
- SlashInvariantForm.instAddCommGroup = Function.Injective.addCommGroup (fun (f : SlashInvariantForm Γ k) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
def
SlashInvariantForm.coeHom
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
SlashInvariantForm Γ k →+ UpperHalfPlane → ℂ
Additive coercion from SlashInvariantForm
to ℍ → ℂ
.
Equations
- SlashInvariantForm.coeHom = { toFun := fun (f : SlashInvariantForm Γ k) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
SlashInvariantForm.coeHom_injective
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Function.Injective ⇑SlashInvariantForm.coeHom
instance
SlashInvariantForm.instModuleComplex
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Module ℂ (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instModuleComplex = Function.Injective.module ℂ SlashInvariantForm.coeHom ⋯ ⋯
@[simp]
theorem
SlashInvariantForm.const_toFun
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
(x : ℂ)
:
The SlashInvariantForm
corresponding to Function.const _ x
.
Equations
- SlashInvariantForm.const x = { toFun := Function.const UpperHalfPlane x, slash_action_eq' := ⋯ }
Instances For
instance
SlashInvariantForm.instOneOfNatInt
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
:
One (SlashInvariantForm Γ 0)
Equations
- SlashInvariantForm.instOneOfNatInt = { one := let __src := SlashInvariantForm.const 1; { toFun := 1, slash_action_eq' := ⋯ } }
@[simp]
theorem
SlashInvariantForm.one_coe_eq_one
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
:
⇑1 = 1
instance
SlashInvariantForm.instInhabited
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
:
Inhabited (SlashInvariantForm Γ k)
Equations
- SlashInvariantForm.instInhabited = { default := 0 }
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₂)
:
instance
SlashInvariantForm.instNatCastOfNatInt
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))
:
NatCast (SlashInvariantForm Γ 0)
Equations
- SlashInvariantForm.instNatCastOfNatInt Γ = { natCast := fun (n : ℕ) => SlashInvariantForm.const ↑n }
@[simp]
theorem
SlashInvariantForm.coe_natCast
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
(n : ℕ)
:
⇑↑n = ↑n
instance
SlashInvariantForm.instIntCastOfNatInt
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))
:
IntCast (SlashInvariantForm Γ 0)
Equations
- SlashInvariantForm.instIntCastOfNatInt Γ = { intCast := fun (z : ℤ) => SlashInvariantForm.const ↑z }
@[simp]
theorem
SlashInvariantForm.coe_intCast
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
(z : ℤ)
:
⇑↑z = ↑z