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) [Group G] [AddMonoid α] [SMul γ α] : Type (max (max u_1 u_2) u_3)

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

• map : β → G → α → α
• zero_slash (k : β) (g : G) : map γ k g 0 = 0
• slash_one (k : β) (a : α) : map γ k 1 a = a
• slash_mul (k : β) (g h : G) (a : α) : map γ k (g * h) a = map γ k h (map γ k g a)
• add_slash (k : β) (g : G) (a b : α) : map γ k g (a + b) = map γ k g a + map γ k g b

def ModularForm.«term_∣[_;_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ModularForm.«term_∣[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SlashAction.neg_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [Group G] [AddGroup α] [SMul γ α] [SlashAction β G α γ] (k : β) (g : G) (a : α) : map γ k g (-a) = -map γ k g a

def monoidHomSlashAction {β : Type u_1} {G : Type u_2} {H : Type u_3} {α : Type u_4} {γ : Type u_5} [Group G] [AddMonoid α] [SMul γ α] [Group H] [SlashAction β G α γ] (h : H →* G) : SlashAction β H α γ

Slash_action induced by a monoid homomorphism.

Equations

• monoidHomSlashAction h = { map := fun (k : β) (g : H) => SlashAction.map γ k (h g), zero_slash := ⋯, slash_one := ⋯, slash_mul := ⋯, add_slash := ⋯ }

def ModularForm.slash (k : ℤ) (γ : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (x : UpperHalfPlane) : ℂ

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

Equations

• ModularForm.slash k γ f x = (UpperHalfPlane.σ γ) (f (γ • x)) * ↑↑(Matrix.GeneralLinearGroup.det γ) ^ (k - 1) * UpperHalfPlane.denom γ ↑x ^ (-k)

instance ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex : SlashAction ℤ (GL (Fin 2) ℝ) (UpperHalfPlane → ℂ) ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem ModularForm.slash_def {k : ℤ} (f : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ) : SlashAction.map ℂ k g f = fun (τ : UpperHalfPlane) => (UpperHalfPlane.σ g) (f (g • τ)) * ↑↑(Matrix.GeneralLinearGroup.det g) ^ (k - 1) * UpperHalfPlane.denom g ↑τ ^ (-k)

theorem ModularForm.slash_apply {k : ℤ} (f : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane) : SlashAction.map ℂ k g f τ = (UpperHalfPlane.σ g) (f (g • τ)) * ↑↑(Matrix.GeneralLinearGroup.det g) ^ (k - 1) * UpperHalfPlane.denom g ↑τ ^ (-k)

theorem ModularForm.smul_slash (k : ℤ) (A : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (c : ℂ) : SlashAction.map ℂ k A (c • f) = (UpperHalfPlane.σ A) c • SlashAction.map ℂ k A f

instance ModularForm.SLAction : SlashAction ℤ (Matrix.SpecialLinearGroup (Fin 2) ℤ) (UpperHalfPlane → ℂ) ℂ

Equations

• ModularForm.SLAction = monoidHomSlashAction (Matrix.SpecialLinearGroup.toGL.comp (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)))

theorem ModularForm.SL_slash {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ k γ f = SlashAction.map ℂ k (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) f

theorem ModularForm.SL_slash_def {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ k γ f = fun (τ : UpperHalfPlane) => f (γ • τ) * UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

theorem ModularForm.SL_slash_apply {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : SlashAction.map ℂ k γ f τ = f (γ • τ) * UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

@[simp]

theorem ModularForm.SL_smul_slash {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (k : ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : UpperHalfPlane → ℂ) (c : α) : SlashAction.map ℂ k A (c • f) = c • SlashAction.map ℂ k A f

theorem ModularForm.is_invariant_const (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : ℂ) : SlashAction.map ℂ 0 A (Function.const UpperHalfPlane x) = Function.const UpperHalfPlane x

theorem ModularForm.is_invariant_one (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ 0 A 1 = 1

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

@[simp]

theorem ModularForm.is_invariant_one' (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ 0 (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 = 1

Variant of is_invariant_one with the left hand side in simp normal form.

theorem ModularForm.slash_action_eq'_iff (k : ℤ) (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (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 : GL (Fin 2) ℝ) (f g : UpperHalfPlane → ℂ) : SlashAction.map ℂ (k1 + k2) A (f * g) = ↑(Matrix.GeneralLinearGroup.det A) • (SlashAction.map ℂ k1 A f * SlashAction.map ℂ k2 A g)

theorem ModularForm.mul_slash_SL2 (k1 k2 : ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f g : UpperHalfPlane → ℂ) : SlashAction.map ℂ (k1 + k2) A (f * g) = SlashAction.map ℂ k1 A f * SlashAction.map ℂ k2 A g