Slash actions #
This file defines a class of slash actions, which are families of right actions of a group on an a
additive monoid, parametrized by some index type. This is modeled on the slash action of
GL (Fin 2) ℝ
on the space of modular forms.
Notation #
Scoped in the ModularForm
namespace, this file defines
f ∣[k] A
: thek
th slash action byA
onf
A general version of the slash action of the space of modular forms. This is the same data as a
family of DistribMulAction Gᵒᵖ α
indexed by k
.
- map : β → G → α → α
Instances
Equations
- One or more equations did not get rendered due to their size.
Instances For
Slash_action induced by a monoid homomorphism.
Equations
- monoidHomSlashAction h = { map := fun (k : β) (g : H) => SlashAction.map k (h g), zero_slash := ⋯, slash_one := ⋯, slash_mul := ⋯, add_slash := ⋯ }
Instances For
Alias of _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash
.
The weight k
action of GL (Fin 2) ℝ
on functions f : ℍ → ℂ
. Invoking this directly is
deprecated; it should always be used via the SlashAction
instance.
Equations
Instances For
The weight k
action of GL (Fin 2) ℝ
on functions f : ℍ → ℂ
.
Equations
- One or more equations did not get rendered due to their size.
The constant function 1 is invariant under any element of SL(2, ℤ)
.
Variant of is_invariant_one
with the left-hand side in simp normal form.
A function f : ℍ → ℂ
is slash-invariant, of weight k ∈ ℤ
and level Γ
,
if for every matrix γ ∈ Γ
we have f(γ • z)= (c*z+d)^k f(z)
where γ= ![![a, b], ![c, d]]
,
and it acts on ℍ
via Möbius transformations.