mathlib documentation

number_theory.modular_forms.slash_actions

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)

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
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 : ℍ → ℂ.

Equations
@[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 : α) :
@[simp]
theorem modular_form.zero_slash (k : ) (A : (matrix.GL_pos (fin 2) )) :
@[simp]

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) :
slash_action.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.