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 ℤ) : Type

Functions ℍ → ℂ that are invariant under the SlashAction.

• toFun : UpperHalfPlane → ℂ

  The underlying function ℍ → ℂ.

  Do NOT use directly. Use the coercion instead.

• slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ self.toFun = self.toFun

class SlashInvariantFormClass (F : Type u_1) (Γ : outParam (Subgroup (GL (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) (γ : GL (Fin 2) ℝ) : γ ∈ Γ → SlashAction.map k γ ⇑f = ⇑f

@[instance 100]

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

def SlashInvariantForm.Simps.coe (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) (k : outParam ℤ) (f : SlashInvariantForm Γ k) : UpperHalfPlane → ℂ

See note [custom simps projection].

@[instance 100]

instance SlashInvariantFormClass.slashInvariantForm (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) (k : outParam ℤ) : SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k

@[simp]

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

@[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) : SlashInvariantForm Γ k

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

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) ℝ) (hγ : γ ∈ Γ) : 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) ℝ} (hγ : γ ∈ Γ) (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) ℝ} (hγ : γ ∈ Γ) (z : UpperHalfPlane) : f (γ • z) = UpperHalfPlane.denom γ ↑z ^ k * f z

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

theorem SlashInvariantForm.slash_action_eqn_SL'' {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) 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 (GL (Fin 2) ℝ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] : CoeTC F (SlashInvariantForm Γ k)

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

@[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

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

@[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 α ℂ ℂ] : SMul α (SlashInvariantForm Γ k)

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

@[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 α ℝ ℂ] : SMul α (SlashInvariantForm Γ k)

Scalar multiplication by ℝ, valid without restrictions on the determinant.

@[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

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

@[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

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

@[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

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

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

Additive coercion from SlashInvariantForm to ℍ → ℂ.

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

instance SlashInvariantForm.instModuleComplex {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] {α : Type u_2} [Semiring α] [Module α ℂ] [IsScalarTower α ℂ ℂ] : Module α (SlashInvariantForm Γ k)

instance SlashInvariantForm.instModuleReal {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [Semiring α] [Module α ℝ] [Module α ℂ] [IsScalarTower α ℝ ℂ] : Module α (SlashInvariantForm Γ k)

def SlashInvariantForm.const {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (x : ℂ) : SlashInvariantForm Γ 0

The SlashInvariantForm corresponding to Function.const _ x.

@[simp]

theorem SlashInvariantForm.coe_const {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (x : ℂ) : ⇑(const x) = Function.const UpperHalfPlane x

@[deprecated SlashInvariantForm.coe_const (since := "2025-12-06")]

theorem SlashInvariantForm.const_toFun {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (x : ℂ) : ⇑(const x) = Function.const UpperHalfPlane x

Alias of SlashInvariantForm.coe_const.

def SlashInvariantForm.constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (x : ℝ) : SlashInvariantForm Γ 0

The SlashInvariantForm corresponding to Function.const _ x.

@[simp]

theorem SlashInvariantForm.coe_constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (x : ℝ) : ⇑(constℝ x) = Function.const UpperHalfPlane ↑x

@[deprecated SlashInvariantForm.coe_constℝ (since := "2025-12-06")]

theorem SlashInvariantForm.constℝ_toFun {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (x : ℝ) : ⇑(constℝ x) = Function.const UpperHalfPlane ↑x

Alias of SlashInvariantForm.coe_constℝ.

instance SlashInvariantForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : One (SlashInvariantForm Γ 0)

@[simp]

theorem SlashInvariantForm.one_coe_eq_one {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : ⇑1 = 1

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

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₂.

@[simp]

theorem SlashInvariantForm.coe_mul {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : SlashInvariantForm Γ k₁) (g : SlashInvariantForm Γ k₂) : ⇑(f.mul g) = ⇑f * ⇑g

def SlashInvariantForm.prod {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (f : (i : ι) → SlashInvariantForm Γ (k i)) : SlashInvariantForm Γ m

Given SlashInvariantForm's f i of weight k i for i : ι, define the form which as a function is a product of those indexed by s : Finset ι with weight m = ∑ i ∈ s, k i.

@[simp]

theorem SlashInvariantForm.coe_prod {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (f : (i : ι) → SlashInvariantForm Γ (k i)) : ⇑(prod m hm f) = ∏ i ∈ s, ⇑(f i)

def SlashInvariantForm.prodEqualWeights {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (f : ι → SlashInvariantForm Γ k) : SlashInvariantForm Γ (↑s.card * k)

Given SlashInvariantForm's f i of weight k, define the form which as a function is a product of those indexed by s : Finset ι with weight #s * k.

@[simp]

theorem SlashInvariantForm.coe_prodEqualWeights {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (f : ι → SlashInvariantForm Γ k) : ⇑(prodEqualWeights f) = ∏ i ∈ s, ⇑(f i)

instance SlashInvariantForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : NatCast (SlashInvariantForm Γ 0)

@[simp]

theorem SlashInvariantForm.coe_natCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (n : ℕ) : ⇑↑n = ↑n

instance SlashInvariantForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] : IntCast (SlashInvariantForm Γ 0)

@[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) ℝ) : SlashInvariantForm (ConjAct.toConjAct g⁻¹ • Γ) k

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

@[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