Documentation

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Slash invariant forms #

This file defines functions that are invariant under a SlashAction which forms the basis for defining ModularForm and CuspForm. We prove several instances for such spaces, in particular that they form a module over , and over if the group is contained in SL(2, ℝ).

structure SlashInvariantForm (Γ : outParam (Subgroup (GL (Fin 2) ))) (k : outParam ) :

Functions ℍ → ℂ that are invariant under the SlashAction.

Instances For

    SlashInvariantFormClass F Γ k asserts F is a type of bundled functions that are invariant under the SlashAction.

    Instances
      @[instance 100]
      Equations
      @[simp]
      @[simp]
      theorem SlashInvariantForm.coe_mk {Γ : outParam (Subgroup (GL (Fin 2) ))} {k : outParam } (f : UpperHalfPlane) (hf : γΓ, SlashAction.map k γ f = f) :
      { toFun := f, slash_action_eq' := hf } = f
      theorem SlashInvariantForm.ext {Γ : outParam (Subgroup (GL (Fin 2) ))} {k : outParam } {f g : SlashInvariantForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) :
      f = g
      theorem SlashInvariantForm.ext_iff {Γ : outParam (Subgroup (GL (Fin 2) ))} {k : outParam } {f g : SlashInvariantForm Γ k} :
      f = g ∀ (x : UpperHalfPlane), f x = g x
      def SlashInvariantForm.copy {Γ : outParam (Subgroup (GL (Fin 2) ))} {k : outParam } (f : SlashInvariantForm Γ k) (f' : UpperHalfPlane) (h : f' = f) :

      Copy of a SlashInvariantForm with a new toFun equal to the old one. Useful to fix definitional equalities.

      Equations
      • f.copy f' h = { toFun := f', slash_action_eq' := }
      Instances For
        theorem SlashInvariantForm.slash_action_eqn {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} {k : } [FunLike F UpperHalfPlane ] [SlashInvariantFormClass F Γ k] (f : F) (γ : GL (Fin 2) ) ( : γ Γ) :
        SlashAction.map k γ f = f
        theorem SlashInvariantForm.slash_action_eqn' {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} [FunLike F UpperHalfPlane ] {k : } [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) } ( : γ Γ) (z : UpperHalfPlane) :
        f (γ z) = ((γ 1 0) * z + (γ 1 1)) ^ k * f z
        theorem SlashInvariantForm.slash_action_eqn'' {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} [FunLike F UpperHalfPlane ] {k : } [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) } ( : γ Γ) (z : UpperHalfPlane) :
        f (γ z) = UpperHalfPlane.denom γ z ^ k * f z

        Every SlashInvariantForm f satisfies f (γ • z) = (denom γ z) ^ k * f z.

        Equations
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_add {Γ : Subgroup (GL (Fin 2) )} {k : } (f g : SlashInvariantForm Γ k) :
        ⇑(f + g) = f + g
        @[simp]
        theorem SlashInvariantForm.add_apply {Γ : Subgroup (GL (Fin 2) )} {k : } (f g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        (f + g) z = f z + g z
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_zero {Γ : Subgroup (GL (Fin 2) )} {k : } :
        0 = 0
        instance SlashInvariantForm.instSMul {Γ : Subgroup (GL (Fin 2) )} {k : } [Γ.HasDetOne] {α : Type u_2} [SMul α ] [IsScalarTower α ] :

        Scalar multiplication by , assuming that Γ ⊆ SL(2, ℝ).

        Equations
        @[simp]
        theorem SlashInvariantForm.coe_smul {Γ : Subgroup (GL (Fin 2) )} {k : } [Γ.HasDetOne] {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) :
        ⇑(n f) = n f
        @[simp]
        theorem SlashInvariantForm.smul_apply {Γ : Subgroup (GL (Fin 2) )} {k : } [Γ.HasDetOne] {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane) :
        (n f) z = n f z
        instance SlashInvariantForm.instSMulℝ {Γ : Subgroup (GL (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [SMul α ] [IsScalarTower α ] :

        Scalar multiplication by , valid without restrictions on the determinant.

        Equations
        @[simp]
        theorem SlashInvariantForm.coe_smulℝ {Γ : Subgroup (GL (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) :
        ⇑(n f) = n f
        @[simp]
        theorem SlashInvariantForm.smul_applyℝ {Γ : Subgroup (GL (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane) :
        (n f) z = n f z
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_neg {Γ : Subgroup (GL (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) :
        ⇑(-f) = -f
        @[simp]
        theorem SlashInvariantForm.neg_apply {Γ : Subgroup (GL (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        (-f) z = -f z
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_sub {Γ : Subgroup (GL (Fin 2) )} {k : } (f g : SlashInvariantForm Γ k) :
        ⇑(f - g) = f - g
        @[simp]
        theorem SlashInvariantForm.sub_apply {Γ : Subgroup (GL (Fin 2) )} {k : } (f g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        (f - g) z = f z - g z

        Additive coercion from SlashInvariantForm to ℍ → ℂ.

        Equations
        Instances For

          The SlashInvariantForm corresponding to Function.const _ x.

          Equations
          Instances For

            The SlashInvariantForm corresponding to Function.const _ x.

            Equations
            Instances For
              def SlashInvariantForm.mul {Γ : Subgroup (GL (Fin 2) )} [Γ.HasDetPlusMinusOne] {k₁ k₂ : } (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
              SlashInvariantForm Γ (k₁ + k₂)

              The slash invariant form of weight k₁ + k₂ given by the product of two slash-invariant forms of weights k₁ and k₂.

              Equations
              • f.mul g = { toFun := f * g, slash_action_eq' := }
              Instances For
                @[simp]
                theorem SlashInvariantForm.coe_mul {Γ : Subgroup (GL (Fin 2) )} [Γ.HasDetPlusMinusOne] {k₁ k₂ : } (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
                (f.mul g) = f * g
                @[simp]
                theorem SlashInvariantForm.coe_natCast {Γ : Subgroup (GL (Fin 2) )} [Γ.HasDetPlusMinusOne] (n : ) :
                n = n
                @[simp]
                theorem SlashInvariantForm.coe_intCast {Γ : Subgroup (GL (Fin 2) )} [Γ.HasDetPlusMinusOne] (z : ) :
                z = z
                noncomputable def SlashInvariantForm.translate {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} {k : } [FunLike F UpperHalfPlane ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ) :

                Translating a SlashInvariantForm by g : GL (Fin 2) ℝ, to obtain a new SlashInvariantForm of level g⁻¹ Γ g.

                Equations
                Instances For
                  @[simp]
                  theorem SlashInvariantForm.coe_translate {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} {k : } [FunLike F UpperHalfPlane ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ) :
                  (translate f g) = SlashAction.map k g f
                  @[deprecated SlashInvariantForm.translate (since := "2025-08-15")]

                  Alias of SlashInvariantForm.translate.


                  Translating a SlashInvariantForm by g : GL (Fin 2) ℝ, to obtain a new SlashInvariantForm of level g⁻¹ Γ g.

                  Equations
                  Instances For
                    @[deprecated SlashInvariantForm.coe_translate (since := "2025-08-15")]
                    theorem SlashInvariantForm.coe_translateGL {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} {k : } [FunLike F UpperHalfPlane ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ) :
                    (translate f g) = SlashAction.map k g f

                    Alias of SlashInvariantForm.coe_translate.

                    @[deprecated SlashInvariantForm.translate (since := "2025-05-15")]

                    Alias of SlashInvariantForm.translate.


                    Translating a SlashInvariantForm by g : GL (Fin 2) ℝ, to obtain a new SlashInvariantForm of level g⁻¹ Γ g.

                    Equations
                    Instances For
                      @[deprecated SlashInvariantForm.coe_translate (since := "2025-05-15")]
                      theorem SlashInvariantForm.coe_translateGLPos {F : Type u_1} {Γ : Subgroup (GL (Fin 2) )} {k : } [FunLike F UpperHalfPlane ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ) :
                      (translate f g) = SlashAction.map k g f

                      Alias of SlashInvariantForm.coe_translate.