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), SlashAction.map γ k g 0 = 0
• slash_one : ∀ (k : β) (a : α), SlashAction.map γ k 1 a = a
• slash_mul : ∀ (k : β) (g h : G) (a : α), SlashAction.map γ k (g * h) a = SlashAction.map γ k h (SlashAction.map γ k g a)
• smul_slash : ∀ (k : β) (g : G) (a : α) (z : γ), SlashAction.map γ k g (z • a) = z • SlashAction.map γ k g a
• add_slash : ∀ (k : β) (g : G) (a b : α), SlashAction.map γ k g (a + b) = SlashAction.map γ k g a + SlashAction.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 : α) : SlashAction.map γ k g (-a) = -SlashAction.map γ k g a

@[simp]

theorem SlashAction.smul_slash_of_tower {R : Type u_1} {β : Type u_2} {G : Type u_3} {α : Type u_4} (γ : Type u_5) [Group G] [AddGroup α] [Monoid γ] [MulAction γ α] [SMul R γ] [SMul R α] [IsScalarTower R γ α] [SlashAction β G α γ] (k : β) (g : G) (a : α) (r : R) : SlashAction.map γ k g (r • a) = r • SlashAction.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 := ⋯, smul_slash := ⋯, add_slash := ⋯ }

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

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

Equations

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

instance ModularForm.instSlashActionIntSubtypeGeneralLinearGroupFinOfNatNatInstOfNatNatRealInstDecidableEqFinFintypeToCommRingToStrictOrderedCommRingLinearOrderedCommRingMemSubgroupInstGroupMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPosForAllUpperHalfPlaneComplexToGroupAddMonoidToAddMonoidToAddMonoidWithOneAddGroupWithOneInstSMulToSMulInstCommSemiringComplexInstSemiringComplexToAlgebraInstNormedFieldComplexToSeminormedRingToSeminormedCommRingToNormedCommRingId : SlashAction ℤ (↥(Matrix.GLPos (Fin 2) ℝ)) (UpperHalfPlane → ℂ) ℂ

Equations

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

theorem ModularForm.slash_def {k : ℤ} (f : UpperHalfPlane → ℂ) (A : ↥(Matrix.GLPos (Fin 2) ℝ)) : SlashAction.map ℂ k A f = ModularForm.slash k A f

instance ModularForm.subgroupAction (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : SlashAction ℤ (↥Γ) (UpperHalfPlane → ℂ) ℂ

Equations

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

@[simp]

theorem ModularForm.subgroup_slash {k : ℤ} (f : UpperHalfPlane → ℂ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (γ : ↥Γ) : SlashAction.map ℂ k γ f = SlashAction.map ℂ k (↑↑γ) f

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

Equations

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

@[simp]

theorem ModularForm.SL_slash {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map ℂ k γ f = SlashAction.map ℂ k (↑γ) 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, ℤ).

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

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