Slash actions #
This file defines a class of slash actions, which are families of right actions of a given group
parametrized by some Type. This is modeled on the slash action of GL_pos (fin 2) ℝ
on the space
of modular forms.
@[class]
structure
slash_action
(β : Type u_1)
(G : Type u_2)
(α : Type u_3)
(γ : Type u_4)
[group G]
[has_zero α]
[has_smul γ α]
[has_add α] :
Type (max u_1 u_2 u_3)
- map : β → G → α → α
- zero_slash : ∀ (k : β) (g : G), slash_action.map γ k g 0 = 0
- slash_one : ∀ (k : β) (a : α), slash_action.map γ k 1 a = a
- right_action : ∀ (k : β) (g h : G) (a : α), slash_action.map γ k h (slash_action.map γ k g a) = slash_action.map γ k (g * h) a
- smul_action : ∀ (k : β) (g : G) (a : α) (z : γ), slash_action.map γ k g (z • a) = z • slash_action.map γ k g a
- add_action : ∀ (k : β) (g : G) (a b : α), slash_action.map γ k g (a + b) = slash_action.map γ k g a + slash_action.map γ k g b
A general version of the slash action of the space of modular forms.
Instances of this typeclass
Instances of other typeclasses for slash_action
- slash_action.has_sizeof_inst
def
monoid_hom_slash_action
{β : Type u_1}
{G : Type u_2}
{H : Type u_3}
{α : Type u_4}
{γ : Type u_5}
[group G]
[has_zero α]
[has_smul γ α]
[has_add α]
[group H]
[slash_action β G α γ]
(h : H →* G) :
slash_action β H α γ
Slash_action induced by a monoid homomorphism.
Equations
- monoid_hom_slash_action h = {map := λ (k : β) (g : H), slash_action.map γ k (⇑h g), zero_slash := _, slash_one := _, right_action := _, smul_action := _, add_action := _}
noncomputable
def
modular_form.slash
(k : ℤ)
(γ : ↥(matrix.GL_pos (fin 2) ℝ))
(f : upper_half_plane → ℂ)
(x : upper_half_plane) :
The weight k
action of GL(2, ℝ)⁺
on functions f : ℍ → ℂ
.
theorem
modular_form.slash_right_action
(k : ℤ)
(A B : ↥(matrix.GL_pos (fin 2) ℝ))
(f : upper_half_plane → ℂ) :
modular_form.slash k B (modular_form.slash k A f) = modular_form.slash k (A * B) f
@[simp]
theorem
modular_form.slash_add
(k : ℤ)
(A : ↥(matrix.GL_pos (fin 2) ℝ))
(f g : upper_half_plane → ℂ) :
modular_form.slash k A (f + g) = modular_form.slash k A f + modular_form.slash k A g
@[simp]
@[simp]
theorem
modular_form.smul_slash
{α : Type u_1}
[has_smul α ℂ]
[is_scalar_tower α ℂ ℂ]
(k : ℤ)
(A : ↥(matrix.GL_pos (fin 2) ℝ))
(f : upper_half_plane → ℂ)
(c : α) :
modular_form.slash k A (c • f) = c • modular_form.slash k A f
@[simp]
theorem
modular_form.neg_slash
(k : ℤ)
(A : ↥(matrix.GL_pos (fin 2) ℝ))
(f : upper_half_plane → ℂ) :
modular_form.slash k A (-f) = -modular_form.slash k A f
@[simp]
theorem
modular_form.zero_slash
(k : ℤ)
(A : ↥(matrix.GL_pos (fin 2) ℝ)) :
modular_form.slash k A 0 = 0
@[protected, instance]
noncomputable
def
modular_form.complex.slash_action
:
slash_action ℤ ↥(matrix.GL_pos (fin 2) ℝ) (upper_half_plane → ℂ) ℂ
Equations
- modular_form.complex.slash_action = {map := modular_form.slash, zero_slash := modular_form.zero_slash, slash_one := modular_form.slash_one, right_action := modular_form.slash_right_action, smul_action := modular_form.complex.slash_action._proof_1, add_action := modular_form.slash_add}
@[protected, instance]
noncomputable
def
modular_form.subgroup_action
(Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :
slash_action ℤ ↥Γ (upper_half_plane → ℂ) ℂ
@[simp]
theorem
modular_form.subgroup_slash
{k : ℤ}
(f : upper_half_plane → ℂ)
(Γ : subgroup (matrix.special_linear_group (fin 2) ℤ))
(γ : ↥Γ) :
slash_action.map ℂ k γ f = modular_form.slash k ↑γ f
@[protected, instance]
noncomputable
def
modular_form.SL_action
:
slash_action ℤ (matrix.special_linear_group (fin 2) ℤ) (upper_half_plane → ℂ) ℂ
@[simp]
theorem
modular_form.SL_slash
{k : ℤ}
(f : upper_half_plane → ℂ)
(γ : matrix.special_linear_group (fin 2) ℤ) :
slash_action.map ℂ k γ f = modular_form.slash k ↑γ f
@[simp]
theorem
modular_form.is_invariant_one
(A : matrix.special_linear_group (fin 2) ℤ) :
slash_action.map ℂ 0 A 1 = 1
The constant function 1 is invariant under any element of SL(2, ℤ)
.
theorem
modular_form.slash_action_eq'_iff
(k : ℤ)
(Γ : subgroup (matrix.special_linear_group (fin 2) ℤ))
(f : upper_half_plane → ℂ)
(γ : ↥Γ)
(z : upper_half_plane) :
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.
theorem
modular_form.mul_slash
(k1 k2 : ℤ)
(A : ↥(matrix.GL_pos (fin 2) ℝ))
(f g : upper_half_plane → ℂ) :
slash_action.map ℂ (k1 + k2) A (f * g) = ↑A.det • slash_action.map ℂ k1 A f * slash_action.map ℂ k2 A g
@[simp]
theorem
modular_form.mul_slash_SL2
(k1 k2 : ℤ)
(A : matrix.special_linear_group (fin 2) ℤ)
(f g : upper_half_plane → ℂ) :
slash_action.map ℂ (k1 + k2) A (f * g) = slash_action.map ℂ k1 A f * slash_action.map ℂ k2 A g
theorem
modular_form.mul_slash_subgroup
(k1 k2 : ℤ)
(Γ : subgroup (matrix.special_linear_group (fin 2) ℤ))
(A : ↥Γ)
(f g : upper_half_plane → ℂ) :
slash_action.map ℂ (k1 + k2) A (f * g) = slash_action.map ℂ k1 A f * slash_action.map ℂ k2 A g