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_reducible, instance 100]

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

Equations

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

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

See note [custom simps projection].

Equations

• SlashInvariantForm.Simps.coe Γ k f = ⇑f

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

Equations

• f.copy f' h = { toFun := f', slash_action_eq' := ⋯ }

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_reducible]

instance SlashInvariantForm.instCoeTCOfSlashInvariantFormClass {F : Type u_1} {Γ : Subgroup (GL (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_reducible]

instance SlashInvariantForm.instAdd {Γ : Subgroup (GL (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 (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_reducible]

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

Equations

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

@[simp]

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

@[instance_reducible]

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

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

Equations

• SlashInvariantForm.instSMul = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c • ⇑f, slash_action_eq' := ⋯ } }

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

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.

Equations

• SlashInvariantForm.instSMulℝ = { smul := fun (c : α) (f : SlashInvariantForm Γ k) => { toFun := c • ⇑f, slash_action_eq' := ⋯ } }

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

instance SlashInvariantForm.instNeg {Γ : Subgroup (GL (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 (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_reducible]

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

Equations

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

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

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

Equations

• SlashInvariantForm.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def SlashInvariantForm.coeHom {Γ : Subgroup (GL (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 (GL (Fin 2) ℝ)} {k : ℤ} : Function.Injective ⇑coeHom

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• SlashInvariantForm.instModuleReal = Function.Injective.module α SlashInvariantForm.coeHom ⋯ ⋯

def SlashInvariantForm.const {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (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.coe_const {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (x : ℂ) : ⇑(const x) = Function.const UpperHalfPlane x

def SlashInvariantForm.constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (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.coe_constℝ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (x : ℝ) : ⇑(constℝ x) = Function.const UpperHalfPlane ↑x

@[instance_reducible]

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

Equations

• SlashInvariantForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal = { one := have __src := SlashInvariantForm.constℝ 1; { toFun := 1, slash_action_eq' := ⋯ } }

@[simp]

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

@[instance_reducible]

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

Equations

• SlashInvariantForm.instInhabited = { default := 0 }

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

Equations

• f.mul g = { toFun := ⇑f * ⇑g, slash_action_eq' := ⋯ }

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

Equations

• SlashInvariantForm.prod m hm f = { toFun := ∏ i ∈ s, ⇑(f i), slash_action_eq' := ⋯ }

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

Equations

• SlashInvariantForm.prodEqualWeights f = SlashInvariantForm.prod (↑s.card * k) ⋯ f

@[simp]

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[instance_reducible]

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

Equations

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

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

Equations

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

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