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

      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

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

        Equations
        Equations
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_smul {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) :
        (n f) = n f
        @[simp]
        theorem SlashInvariantForm.smul_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } {α : Type u_2} [SMul α ] [IsScalarTower α ] (f : SlashInvariantForm Γ k) (n : α) (z : UpperHalfPlane) :
        (n f) z = n f z
        Equations

        Additive coercion from SlashInvariantForm to ℍ → ℂ.

        Equations
        Instances For

          The SlashInvariantForm corresponding to Function.const _ x.

          Equations
          Instances For
            Equations

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

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