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

@[simp]

theorem SlashAction.sum_slash {β : Type u_1} {G : Type u_2} {α : Type u_3} {ι : Type u_4} [Monoid G] [AddCommGroup α] [SlashAction β G α] (k : β) (g : G) {a : ι → α} {s : Finset ι} : map k g (∑ i ∈ s, a i) = ∑ i ∈ s, map k g (a i)

@[instance_reducible]

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 α

SlashAction 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 := ⋯ }

@[simp]

theorem SlashAction.slash_eq_zero_iff {β : Type u_1} {G : Type u_2} {α : Type u_3} [Group G] [AddGroup α] [SlashAction β G α] (k : β) (g : G) (a : α) : map k g a = 0 ↔ a = 0

@[instance_reducible]

noncomputable 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_reducible]

noncomputable 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

theorem ModularForm.div_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

theorem ModularForm.prod_slash_sum_weights {ι : Type u_1} {k : ι → ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι} : SlashAction.map (∑ i ∈ s, k i) g (∏ i ∈ s, f i) = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map (k i) g (f i)

theorem ModularForm.prod_slash {ι : Type u_1} {k : ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι} : SlashAction.map (k * ↑s.card) g (∏ i ∈ s, f i) = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map k g (f i)

@[deprecated ModularForm.prod_slash (since := "2026-01-22")]

theorem ModularForm.prod_fintype_slash {ι : Type u_1} [Fintype ι] [Nonempty ι] {k : ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} : SlashAction.map (k * ↑(Fintype.card ι)) g (∏ i : ι, f i) = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i : ι, SlashAction.map k g (f i)