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
      theorem SlashInvariantFormClass.slash_action_eq {F : Type u_1} {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } :
      ∀ {inst : FunLike F UpperHalfPlane } [self : SlashInvariantFormClass F Γ k] (f : F), γΓ, SlashAction.map k γ f = f
      @[instance 100]
      Equations
      @[simp]
      theorem SlashInvariantForm.coe_mk {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ))} {k : outParam } (f : UpperHalfPlane) (hf : γΓ, 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.

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

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

        Equations
        • SlashInvariantForm.instCoeTCOfSlashInvariantFormClass = { coe := fun (f : F) => { toFun := f, slash_action_eq' := } }
        Equations
        • SlashInvariantForm.instAdd = { add := fun (f g : SlashInvariantForm Γ k) => { toFun := f + g, slash_action_eq' := } }
        @[simp]
        theorem SlashInvariantForm.coe_add {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) :
        (f + g) = f + g
        @[simp]
        theorem SlashInvariantForm.add_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        (f + g) z = f z + g z
        Equations
        • SlashInvariantForm.instZero = { zero := { toFun := 0, slash_action_eq' := } }
        Equations
        • SlashInvariantForm.instSMul = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c f, slash_action_eq' := } }
        @[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
        • SlashInvariantForm.instNeg = { neg := fun (f : SlashInvariantForm Γ k) => { toFun := -f, slash_action_eq' := } }
        @[simp]
        Equations
        @[simp]
        theorem SlashInvariantForm.coe_sub {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) :
        (f - g) = f - g
        @[simp]
        theorem SlashInvariantForm.sub_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )} {k : } (f : SlashInvariantForm Γ k) (g : SlashInvariantForm Γ k) (z : UpperHalfPlane) :
        (f - g) z = f z - g z
        Equations

        Additive coercion from SlashInvariantForm to ℍ → ℂ.

        Equations
        • SlashInvariantForm.coeHom = { toFun := fun (f : SlashInvariantForm Γ k) => f, map_zero' := , map_add' := }
        Instances For
          Equations

          The SlashInvariantForm corresponding to Function.const _ x.

          Equations
          Instances For
            Equations
            • SlashInvariantForm.instOneOfNatInt = { one := let __src := SlashInvariantForm.const 1; { toFun := 1, slash_action_eq' := } }
            Equations
            • SlashInvariantForm.instInhabited = { default := 0 }
            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₂.

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