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.
Functions ℍ → ℂ
that are invariant under the SlashAction
.
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map ℂ k γ self.toFun = self.toFun
Instances For
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
Equations
- SlashInvariantForm.funLike Γ k = { coe := SlashInvariantForm.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
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
Every SlashInvariantForm
f
satisfies f (γ • z) = (denom γ z) ^ k * f z
.
Equations
- SlashInvariantForm.instCoeTCOfSlashInvariantFormClass = { coe := fun (f : F) => { toFun := ⇑f, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instAdd = { add := fun (f g : SlashInvariantForm Γ k) => { toFun := ⇑f + ⇑g, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instZero = { zero := { toFun := 0, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instSMul = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c • ⇑f, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instNeg = { neg := fun (f : SlashInvariantForm Γ k) => { toFun := -⇑f, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instSub = { sub := fun (f g : SlashInvariantForm Γ k) => f + -g }
Equations
- SlashInvariantForm.instAddCommGroup = Function.Injective.addCommGroup (fun (f : SlashInvariantForm Γ k) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Additive coercion from SlashInvariantForm
to ℍ → ℂ
.
Equations
- SlashInvariantForm.coeHom = { toFun := fun (f : SlashInvariantForm Γ k) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- SlashInvariantForm.instModuleComplex = Function.Injective.module ℂ SlashInvariantForm.coeHom ⋯ ⋯
The SlashInvariantForm
corresponding to Function.const _ x
.
Equations
- SlashInvariantForm.const x = { toFun := Function.const UpperHalfPlane x, slash_action_eq' := ⋯ }
Instances For
Equations
- SlashInvariantForm.instOneOfNatInt = { one := let __src := SlashInvariantForm.const 1; { toFun := 1, slash_action_eq' := ⋯ } }
Equations
- SlashInvariantForm.instInhabited = { default := 0 }
The slash invariant form of weight k₁ + k₂
given by the product of two modular forms of
weights k₁
and k₂
.
Instances For
Equations
- SlashInvariantForm.instNatCastOfNatInt Γ = { natCast := fun (n : ℕ) => SlashInvariantForm.const ↑n }
Equations
- SlashInvariantForm.instIntCastOfNatInt Γ = { intCast := fun (z : ℤ) => SlashInvariantForm.const ↑z }