Slash actions

This file defines a class of slash actions, which are families of right actions of a group on an a additive monoid, parametrized by some index type. This is modeled on the slash action of GL (Fin 2) ℝ on the space of modular forms.

Notation

Scoped in the ModularForm namespace, this file defines

• f ∣[k] A: the kth slash action by A on f

class SlashAction (β : Type u_1) (G : Type u_2) (α : Type u_3) [Monoid G] [AddMonoid α] : Type (max (max u_1 u_2) u_3)

A general version of the slash action of the space of modular forms. This is the same data as a family of DistribMulAction Gᵒᵖ α indexed by k.

• 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.

@[simp]

theorem SlashAction.neg_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} [Monoid G] [AddGroup α] [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} [Monoid G] [AddMonoid α] [Monoid 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 := ⋯ }

@[deprecated _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash (since := "2025-09-19")]

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

Alias of _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash.

---

The weight k action of GL (Fin 2) ℝ on functions f : ℍ → ℂ. Invoking this directly is deprecated; it should always be used via the SlashAction instance.

Equations

• ModularForm.slash = ModularForm.privateSlash✝

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

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

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.mapGL ℝ)

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