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.

structure SlashInvariantForm (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) : Type

Functions ℍ → ℂ that are invariant under the SlashAction.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ Γ → SlashAction.map ℂ k γ self.toFun = self.toFun

class SlashInvariantFormClass (F : Type u_1) (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] : Prop

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

• slash_action_eq (f : F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ Γ → SlashAction.map ℂ k γ ⇑f = ⇑f

@[instance 100]

instance SlashInvariantForm.funLike (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) : FunLike (SlashInvariantForm Γ k) UpperHalfPlane ℂ

Equations

• SlashInvariantForm.funLike Γ k = { coe := SlashInvariantForm.toFun, coe_injective' := ⋯ }

@[instance 100]

instance SlashInvariantFormClass.slashInvariantForm (Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))) (k : outParam ℤ) : SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k

@[simp]

theorem SlashInvariantForm.toFun_eq_coe {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {f : SlashInvariantForm Γ k} : f.toFun = ⇑f

@[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 g : SlashInvariantForm Γ k} (h : ∀ (x : UpperHalfPlane), f x = g x) : f = g

theorem SlashInvariantForm.ext_iff {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} {f g : SlashInvariantForm Γ k} : f = g ↔ ∀ (x : UpperHalfPlane), f x = g x

def SlashInvariantForm.copy {Γ : outParam (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))} {k : outParam ℤ} (f : SlashInvariantForm Γ k) (f' : UpperHalfPlane → ℂ) (h : f' = ⇑f) : SlashInvariantForm Γ k

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' := ⋯ }

theorem SlashInvariantForm.slash_action_eqn {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hγ : γ ∈ Γ) : SlashAction.map ℂ k γ ⇑f = ⇑f

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

theorem SlashInvariantForm.slash_action_eqn'' {F : Type u_2} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [SlashInvariantFormClass F Γ k] (f : F) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ Γ) (z : UpperHalfPlane) : f (γ • z) = UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k * f z

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

instance SlashInvariantForm.instCoeTCOfSlashInvariantFormClass {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] : CoeTC F (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instCoeTCOfSlashInvariantFormClass = { coe := fun (f : F) => { toFun := ⇑f, slash_action_eq' := ⋯ } }

instance SlashInvariantForm.instAdd {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Add (SlashInvariantForm Γ k)

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 g : SlashInvariantForm Γ k) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem SlashInvariantForm.add_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f g : SlashInvariantForm Γ k) (z : UpperHalfPlane) : (f + g) z = f z + g z

instance SlashInvariantForm.instZero {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Zero (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instZero = { zero := { toFun := 0, slash_action_eq' := ⋯ } }

@[simp]

theorem SlashInvariantForm.coe_zero {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : ⇑0 = 0

instance SlashInvariantForm.instSMul {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} {α : Type u_2} [SMul α ℂ] [IsScalarTower α ℂ ℂ] : SMul α (SlashInvariantForm Γ k)

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

instance SlashInvariantForm.instNeg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Neg (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instNeg = { neg := fun (f : SlashInvariantForm Γ k) => { toFun := -⇑f, slash_action_eq' := ⋯ } }

@[simp]

theorem SlashInvariantForm.coe_neg {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : SlashInvariantForm Γ k) : ⇑(-f) = -⇑f

@[simp]

theorem SlashInvariantForm.neg_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : SlashInvariantForm Γ k) (z : UpperHalfPlane) : (-f) z = -f z

instance SlashInvariantForm.instSub {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Sub (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instSub = { sub := fun (f g : SlashInvariantForm Γ k) => f + -g }

@[simp]

theorem SlashInvariantForm.coe_sub {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f g : SlashInvariantForm Γ k) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem SlashInvariantForm.sub_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f g : SlashInvariantForm Γ k) (z : UpperHalfPlane) : (f - g) z = f z - g z

instance SlashInvariantForm.instAddCommGroup {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : AddCommGroup (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instAddCommGroup = Function.Injective.addCommGroup (fun (f : SlashInvariantForm Γ k) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def SlashInvariantForm.coeHom {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : SlashInvariantForm Γ k →+ UpperHalfPlane → ℂ

Additive coercion from SlashInvariantForm to ℍ → ℂ.

Equations

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

theorem SlashInvariantForm.coeHom_injective {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Function.Injective ⇑coeHom

instance SlashInvariantForm.instModuleComplex {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Module ℂ (SlashInvariantForm Γ k)

Equations

• SlashInvariantForm.instModuleComplex = Function.Injective.module ℂ SlashInvariantForm.coeHom ⋯ ⋯

def SlashInvariantForm.const {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (x : ℂ) : SlashInvariantForm Γ 0

The SlashInvariantForm corresponding to Function.const _ x.

Equations

• SlashInvariantForm.const x = { toFun := Function.const UpperHalfPlane x, slash_action_eq' := ⋯ }

@[simp]

theorem SlashInvariantForm.const_toFun {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (x : ℂ) : ⇑(const x) = Function.const UpperHalfPlane x

instance SlashInvariantForm.instOneOfNatInt {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : One (SlashInvariantForm Γ 0)

Equations

• SlashInvariantForm.instOneOfNatInt = { one := let __src := SlashInvariantForm.const 1; { toFun := 1, slash_action_eq' := ⋯ } }

@[simp]

theorem SlashInvariantForm.one_coe_eq_one {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : ⇑1 = 1

instance SlashInvariantForm.instInhabited {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Inhabited (SlashInvariantForm Γ k)

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' := ⋯ }

@[simp]

theorem SlashInvariantForm.coe_mul {k₁ k₂ : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) : ⇑(f.mul g) = ⇑f * ⇑g

instance SlashInvariantForm.instNatCastOfNatInt (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : NatCast (SlashInvariantForm Γ 0)

Equations

• SlashInvariantForm.instNatCastOfNatInt Γ = { natCast := fun (n : ℕ) => SlashInvariantForm.const ↑n }

@[simp]

theorem SlashInvariantForm.coe_natCast {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (n : ℕ) : ⇑↑n = ↑n

instance SlashInvariantForm.instIntCastOfNatInt (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : IntCast (SlashInvariantForm Γ 0)

Equations

• SlashInvariantForm.instIntCastOfNatInt Γ = { intCast := fun (z : ℤ) => SlashInvariantForm.const ↑z }

@[simp]

theorem SlashInvariantForm.coe_intCast {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (z : ℤ) : ⇑↑z = ↑z

noncomputable def SlashInvariantForm.translateGL {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : SlashInvariantForm (CongruenceSubgroup.conjGL Γ g) k

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

Equations

• SlashInvariantForm.translateGL f g = { toFun := SlashAction.map ℂ k g ⇑f, slash_action_eq' := ⋯ }

@[simp]

theorem SlashInvariantForm.coe_translateGL {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : ⇑(translateGL f g) = SlashAction.map ℂ k g ⇑f

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

def SlashInvariantForm.translateGLPos {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : SlashInvariantForm (CongruenceSubgroup.conjGL Γ g) k

Alias of SlashInvariantForm.translateGL.

---

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

Equations

• @SlashInvariantForm.translateGLPos = @SlashInvariantForm.translateGL

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

theorem SlashInvariantForm.coe_translateGLPos {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : ⇑(translateGL f g) = SlashAction.map ℂ k g ⇑f

Alias of SlashInvariantForm.coe_translateGL.

noncomputable def SlashInvariantForm.translate {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashInvariantForm (ConjAct.toConjAct g⁻¹ • Γ) k

Translating a SlashInvariantForm by g : SL(2, ℤ), to obtain a new SlashInvariantForm of level g⁻¹ Γ g.

Equations

• SlashInvariantForm.translate f g = { toFun := SlashAction.map ℂ k g ⇑f, slash_action_eq' := ⋯ }

@[simp]

theorem SlashInvariantForm.coe_translate {F : Type u_1} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ⇑(translate f g) = SlashAction.map ℂ k g ⇑f