mathlib3 documentation


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

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)

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
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 : α) :
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) : γ k g (r a) = r γ 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.

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]

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