Slash actions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Notation #
In the modular_form locale, this provides
f ∣[k;γ] A: thekthγ-compatible slash action byAonff ∣[k] A: thekthℂ-compatible slash action byAonf; a shorthand forf ∣[k;ℂ] A
@[class]
structure
slash_action
(β : Type u_1)
(G : Type u_2)
(α : Type u_3)
(γ : Type u_4)
[group G]
[add_monoid α]
[has_smul γ α] :
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
- slash_mul : ∀ (k : β) (g h : G) (a : α), slash_action.map γ k (g * h) a = slash_action.map γ k h (slash_action.map γ k g a)
- smul_slash : ∀ (k : β) (g : G) (a : α) (z : γ), slash_action.map γ k g (z • a) = z • slash_action.map γ k g a
- add_slash : ∀ (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
@[simp]
theorem
slash_action.neg_slash
{β : Type u_1}
{G : Type u_2}
{α : Type u_3}
{γ : Type u_4}
[group G]
[add_group α]
[has_smul γ α]
[slash_action β G α γ]
(k : β)
(g : G)
(a : α) :
slash_action.map γ k g (-a) = -slash_action.map γ k g a
@[simp]
theorem
slash_action.smul_slash_of_tower
{R : Type u_1}
{β : Type u_2}
{G : Type u_3}
{α : Type u_4}
(γ : Type u_5)
[group G]
[add_group α]
[monoid γ]
[mul_action γ α]
[has_smul R γ]
[has_smul R α]
[is_scalar_tower R γ α]
[slash_action β G α γ]
(k : β)
(g : G)
(a : α)
(r : R) :
slash_action.map γ k g (r • a) = r • slash_action.map γ k g a
def
monoid_hom_slash_action
{β : Type u_1}
{G : Type u_2}
{H : Type u_3}
{α : Type u_4}
{γ : Type u_5}
[group G]
[add_monoid α]
[has_smul γ α]
[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 := _, slash_mul := _, smul_slash := _, add_slash := _}
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 : ℍ → ℂ.
@[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 := zero_slash, slash_one := slash_one, slash_mul := slash_mul, smul_slash := modular_form.complex.slash_action._proof_1, add_slash := add_slash}
theorem
modular_form.slash_def
{k : ℤ}
(f : upper_half_plane → ℂ)
(A : ↥(matrix.GL_pos (fin 2) ℝ)) :
slash_action.map ℂ k A f = modular_form.slash k A f
@[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 = slash_action.map ℂ 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 = slash_action.map ℂ 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