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 over ℝ, and over ℂ if the group is contained in SL(2, ℝ).

structure SlashInvariantForm (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) (k : outParam ℤ) :

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

Instances For

class SlashInvariantFormClass (F : Type u_1) (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) (k : outParam ℤ) [FunLike F UpperHalfPlane ℂ] :

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

Instances

@[implicit_reducible, 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].

Instances For

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

Instances For

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.

@[implicit_reducible]

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

CoeTC F (SlashInvariantForm Γ k)

@[implicit_reducible]

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

@[implicit_reducible]

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

Zero (SlashInvariantForm Γ k)

@[simp]

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

⇑0 = 0

@[implicit_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, ℝ).

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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 ℍ → ℂ.

Instances For

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

Function.Injective ⇑coeHom

@[implicit_reducible]

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

Module α (SlashInvariantForm Γ k)

@[implicit_reducible]

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

Instances For

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

Instances For

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

@[implicit_reducible]

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

@[implicit_reducible]

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

Instances For

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

Instances For

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

Instances For

@[simp]

theorem SlashInvariantForm.coe_prodEqualWeights {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (f : ι → SlashInvariantForm Γ k) :

⇑(prodEqualWeights f) = ∏ i ∈ s, ⇑(f i)

@[implicit_reducible]

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

NatCast (SlashInvariantForm Γ 0)

@[simp]

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

⇑↑n = ↑n

@[implicit_reducible]

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.

Instances For

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