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.

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
      @[simp]
      theorem SlashInvariantForm.coe_mk {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : UpperHalfPlane) (hf : ∀ (γ : { x // x Γ }), SlashAction.map k γ f = f) :
      { toFun := f, slash_action_eq' := hf } = f
      theorem SlashInvariantForm.ext {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } {f : SlashInvariantForm Γ k} {g : SlashInvariantForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) :
      f = g

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

      Instances For
        theorem SlashInvariantForm.slash_action_eqn {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } [SlashInvariantFormClass F Γ k] (f : F) (γ : { x // x Γ }) :
        SlashAction.map k γ f = f
        theorem SlashInvariantForm.slash_action_eqn' {F : Type u_1} (k : ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) [SlashInvariantFormClass F Γ k] (f : F) (γ : { x // x Γ }) (z : UpperHalfPlane) :
        f (γ z) = (↑(γ 1 0) * z + ↑(γ 1 1)) ^ k * f z
        @[simp]
        theorem SlashInvariantForm.SlashInvariantFormClass.coe_coe {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } [SlashInvariantFormClass F Γ k] (f : F) :
        { toFun := f, slash_action_eq' := (_ : ∀ (γ : { x // x Γ }), SlashAction.map k γ f = f) } = f
        @[simp]
        theorem SlashInvariantForm.coe_add {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) :
        ↑(f + g) = f + g
        @[simp]
        theorem SlashInvariantForm.add_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        ↑(f + g) z = f z + g z
        @[simp]
        theorem SlashInvariantForm.coe_smul {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) :
        ↑(n f) = n f
        @[simp]
        theorem SlashInvariantForm.smul_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane) :
        ↑(n f) z = n f z
        @[simp]
        theorem SlashInvariantForm.coe_sub {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) :
        ↑(f - g) = f - g
        @[simp]
        theorem SlashInvariantForm.sub_apply {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        ↑(f - g) z = f z - g z

        Additive coercion from SlashInvariantForm to ℍ → ℂ.

        Instances For
          def SlashInvariantForm.mul {k₁ : } {k₂ : } {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
          SlashInvariantForm Γ (k₁ + k₂)

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

          Instances For
            @[simp]
            theorem SlashInvariantForm.coe_mul {k₁ : } {k₂ : } {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) :
            ↑(SlashInvariantForm.mul f g) = f * g