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
: thek
thγ
-compatible slash action byA
onf
f ∣[k] A
: thek
thℂ
-compatible slash action byA
onf
; a shorthand forf ∣[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)
- 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
A general version of the slash action of the space of modular forms.
Instances
@[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.
Instances For
def
ModularForm.slash
(k : ℤ)
(γ : { x // x ∈ Matrix.GLPos (Fin 2) ℝ })
(f : UpperHalfPlane → ℂ)
(x : UpperHalfPlane)
:
The weight k
action of GL(2, ℝ)⁺
on functions f : ℍ → ℂ
.
Instances For
instance
ModularForm.instSlashActionIntSubtypeGeneralLinearGroupFinOfNatNatInstOfNatNatRealInstDecidableEqFinFintypeToCommRingToStrictOrderedCommRingLinearOrderedCommRingMemSubgroupInstGroupUnitsMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPosForAllUpperHalfPlaneComplexToGroupAddMonoidToAddMonoidToAddMonoidWithOneAddGroupWithOneInstSMulToSMulInstCommSemiringComplexInstSemiringComplexToAlgebraInstNormedFieldComplexToSeminormedRingToSeminormedCommRingToNormedCommRingId :
SlashAction ℤ { x // x ∈ Matrix.GLPos (Fin 2) ℝ } (UpperHalfPlane → ℂ) ℂ
theorem
ModularForm.slash_def
{k : ℤ}
(f : UpperHalfPlane → ℂ)
(A : { x // x ∈ Matrix.GLPos (Fin 2) ℝ })
:
SlashAction.map ℂ k A f = ModularForm.slash k A f
instance
ModularForm.subgroupAction
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))
:
SlashAction ℤ { x // x ∈ Γ } (UpperHalfPlane → ℂ) ℂ
@[simp]
theorem
ModularForm.subgroup_slash
{k : ℤ}
(f : UpperHalfPlane → ℂ)
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))
(γ : { x // x ∈ Γ })
:
SlashAction.map ℂ k γ f = SlashAction.map ℂ k (↑↑γ) f
instance
ModularForm.SLAction :
SlashAction ℤ (Matrix.SpecialLinearGroup (Fin 2) ℤ) (UpperHalfPlane → ℂ) ℂ
@[simp]
theorem
ModularForm.SL_slash
{k : ℤ}
(f : UpperHalfPlane → ℂ)
(γ : Matrix.SpecialLinearGroup (Fin 2) ℤ)
:
SlashAction.map ℂ k γ f = SlashAction.map ℂ k (↑γ) f
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 → ℂ)
(γ : { x // x ∈ Γ })
(z : UpperHalfPlane)
:
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 : { x // x ∈ 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 : { x // x ∈ Γ })
(f : UpperHalfPlane → ℂ)
(g : UpperHalfPlane → ℂ)
:
SlashAction.map ℂ (k1 + k2) A (f * g) = SlashAction.map ℂ k1 A f * SlashAction.map ℂ k2 A g