number_theory.modular_forms.slash_actions

@[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

source

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 := _}

source

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

modular_form.slash k γ f x = f (γ • x) * ↑(↑γ.det) ^ (k - 1) * upper_half_plane.denom γ x ^ -k

source

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

source

@[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

source

@[simp]

theorem modular_form.slash_one (k : ℤ) (f : upper_half_plane → ℂ) :

modular_form.slash k 1 f = f

source

@[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

source

@[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

source

@[simp]

theorem modular_form.zero_slash (k : ℤ) (A : ↥(matrix.GL_pos (fin 2) ℝ)) :

modular_form.slash k A 0 = 0

source

@[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}

source

@[protected, instance]

noncomputable def modular_form.subgroup_action (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :

slash_action ℤ ↥Γ (upper_half_plane → ℂ) ℂ

Equations

modular_form.subgroup_action Γ = monoid_hom_slash_action (matrix.special_linear_group.to_GL_pos.comp ((matrix.special_linear_group.map (int.cast_ring_hom ℝ)).comp Γ.subtype))

source

@[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

source

@[protected, instance]

noncomputable def modular_form.SL_action :

slash_action ℤ (matrix.special_linear_group (fin 2) ℤ) (upper_half_plane → ℂ) ℂ

Equations

modular_form.SL_action = monoid_hom_slash_action (matrix.special_linear_group.to_GL_pos.comp (matrix.special_linear_group.map (int.cast_ring_hom ℝ)))

source

@[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

source

@[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, ℤ).

source

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.

source

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

source

@[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

source

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

mathlib documentation

Slash actions #