Documentation

Mathlib.NumberTheory.ModularForms.SlashActions

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

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
Instances
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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
      Instances For
        @[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
        Instances For

          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 : ) :
          @[simp]
          theorem ModularForm.SL_smul_slash {α : Type u_1} [SMul α ] [IsScalarTower α ] (k : ) (A : Matrix.SpecialLinearGroup (Fin 2) ) (f : UpperHalfPlane) (c : α) :

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

          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) :