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 over ℝ
, and over ℂ
if the group is contained in SL(2, ℝ)
.
Functions ℍ → ℂ
that are invariant under the SlashAction
.
- toFun : UpperHalfPlane → ℂ
The underlying function
ℍ → ℂ
.Do NOT use directly. Use the coercion instead.
Instances For
SlashInvariantFormClass F Γ k
asserts F
is a type of bundled functions that are invariant
under the SlashAction
.
Instances
Equations
- SlashInvariantForm.funLike Γ k = { coe := SlashInvariantForm.toFun, coe_injective' := ⋯ }
Copy of a SlashInvariantForm
with a new toFun
equal to the old one.
Useful to fix definitional equalities.
Instances For
Every SlashInvariantForm
f
satisfies f (γ • z) = (denom γ z) ^ k * f z
.
Every SlashInvariantForm
f
satisfies f (γ • z) = (denom γ z) ^ k * f z
.
Equations
- SlashInvariantForm.instAdd = { add := fun (f g : SlashInvariantForm Γ k) => { toFun := ⇑f + ⇑g, slash_action_eq' := ⋯ } }
Scalar multiplication by ℂ
, assuming that Γ ⊆ SL(2, ℝ)
.
Equations
- SlashInvariantForm.instSMul = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c • ⇑f, slash_action_eq' := ⋯ } }
Scalar multiplication by ℝ
, valid without restrictions on the determinant.
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
The SlashInvariantForm
corresponding to Function.const _ x
.
Equations
- SlashInvariantForm.const x = { toFun := Function.const UpperHalfPlane x, slash_action_eq' := ⋯ }
Instances For
The SlashInvariantForm
corresponding to Function.const _ x
.
Equations
- SlashInvariantForm.constℝ x = { toFun := Function.const UpperHalfPlane ↑x, slash_action_eq' := ⋯ }
Instances For
Equations
- SlashInvariantForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal = { one := have __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 slash-invariant forms
of weights k₁
and k₂
.
Instances For
Equations
- SlashInvariantForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal = { natCast := fun (n : ℕ) => SlashInvariantForm.constℝ ↑n }
Equations
- SlashInvariantForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal = { intCast := fun (z : ℤ) => SlashInvariantForm.constℝ ↑z }
Translating a SlashInvariantForm
by g : GL (Fin 2) ℝ
, to obtain a new
SlashInvariantForm
of level g⁻¹ Γ g
.
Equations
- SlashInvariantForm.translate f g = { toFun := SlashAction.map k g ⇑f, slash_action_eq' := ⋯ }
Instances For
Alias of SlashInvariantForm.translate
.
Translating a SlashInvariantForm
by g : GL (Fin 2) ℝ
, to obtain a new
SlashInvariantForm
of level g⁻¹ Γ g
.
Instances For
Alias of SlashInvariantForm.coe_translate
.
Alias of SlashInvariantForm.translate
.
Translating a SlashInvariantForm
by g : GL (Fin 2) ℝ
, to obtain a new
SlashInvariantForm
of level g⁻¹ Γ g
.
Instances For
Alias of SlashInvariantForm.coe_translate
.