# 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 GLPos (Fin 2) ℝ on the space of modular forms.

## Notation #

In the ModularForm locale, this provides

• f ∣[k;γ] A: the kth γ-compatible slash action by A on f
• f ∣[k] A: the kth ℂ-compatible slash action by A on f; a shorthand for f ∣[k;ℂ] A
class SlashAction (β : Type u_1) (G : Type u_2) (α : Type u_3) (γ : Type u_4) [] [] [SMul γ α] :
Type (max (max u_1 u_2) u_3)

A general version of the slash action of the space of modular forms.

Instances
@[simp]
theorem SlashAction.zero_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [self : SlashAction β G α γ] (k : β) (g : G) :
SlashAction.map γ k g 0 = 0
@[simp]
theorem SlashAction.slash_one {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [self : SlashAction β G α γ] (k : β) (a : α) :
SlashAction.map γ k 1 a = a
theorem SlashAction.slash_mul {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [self : SlashAction β G α γ] (k : β) (g : G) (h : G) (a : α) :
SlashAction.map γ k (g * h) a = SlashAction.map γ k h (SlashAction.map γ k g a)
@[simp]
theorem SlashAction.smul_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [self : SlashAction β G α γ] (k : β) (g : G) (a : α) (z : γ) :
SlashAction.map γ k g (z a) = z SlashAction.map γ k g a
@[simp]
theorem SlashAction.add_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [self : SlashAction β G α γ] (k : β) (g : G) (a : α) (b : α) :
SlashAction.map γ k g (a + b) = SlashAction.map γ k g a + SlashAction.map γ k g b
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SlashAction.neg_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [] [] [SMul γ α] [SlashAction β G α γ] (k : β) (g : G) (a : α) :
SlashAction.map γ k g (-a) = -SlashAction.map γ k g a
@[simp]
theorem SlashAction.smul_slash_of_tower {R : Type u_1} {β : Type u_2} {G : Type u_3} {α : Type u_4} (γ : Type u_5) [] [] [] [] [SMul R γ] [SMul R α] [] [SlashAction β G α γ] (k : β) (g : G) (a : α) (r : R) :
SlashAction.map γ k g (r a) = r SlashAction.map γ k g a
def monoidHomSlashAction {β : Type u_1} {G : Type u_2} {H : Type u_3} {α : Type u_4} {γ : Type u_5} [] [] [SMul γ α] [] [SlashAction β G α γ] (h : H →* G) :
SlashAction β H α γ

Slash_action induced by a monoid homomorphism.

Equations
• = { map := fun (k : β) (g : H) => SlashAction.map γ k (h g), zero_slash := , slash_one := , slash_mul := , smul_slash := , add_slash := }
Instances For
def ModularForm.slash (k : ) (γ : (Matrix.GLPos (Fin 2) )) (f : ) (x : UpperHalfPlane) :

The weight k action of GL(2, ℝ)⁺ on functions f : ℍ → ℂ.

Equations
• = f (γ x) * (γ).det ^ (k - 1) * ^ (-k)
Instances For
Equations
• One or more equations did not get rendered due to their size.
theorem ModularForm.slash_def {k : } (f : ) (A : (Matrix.GLPos (Fin 2) )) :
=
instance ModularForm.subgroupAction (Γ : ) :
SlashAction (Γ) ()
Equations
@[simp]
theorem ModularForm.subgroup_slash {k : } (f : ) (Γ : ) (γ : Γ) :
= SlashAction.map k (γ) f
Equations
@[simp]
theorem ModularForm.SL_slash {k : } (f : ) (γ : ) :
= SlashAction.map k (γ) f
theorem ModularForm.is_invariant_one (A : ) :
= 1

The constant function 1 is invariant under any element of SL(2, ℤ).

theorem ModularForm.slash_action_eq'_iff (k : ) (Γ : ) (f : ) (γ : Γ) (z : UpperHalfPlane) :
SlashAction.map k γ f z = f z f (γ z) = ((γ 1 0) * z + (γ 1 1)) ^ k * f z

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 ModularForm.mul_slash (k1 : ) (k2 : ) (A : (Matrix.GLPos (Fin 2) )) (f : ) (g : ) :
SlashAction.map (k1 + k2) A (f * g) = (A).det SlashAction.map k1 A f * SlashAction.map k2 A g
theorem ModularForm.mul_slash_SL2 (k1 : ) (k2 : ) (A : ) (f : ) (g : ) :
SlashAction.map (k1 + k2) A (f * g) = SlashAction.map k1 A f * SlashAction.map k2 A g
theorem ModularForm.mul_slash_subgroup (k1 : ) (k2 : ) (Γ : ) (A : Γ) (f : ) (g : ) :
SlashAction.map (k1 + k2) A (f * g) = SlashAction.map k1 A f * SlashAction.map k2 A g