Norm and trace maps

Given two subgroups 𝒢, ℋ of GL(2, ℝ) with 𝒢.relindex ℋ ≠ 0 (i.e. 𝒢 ⊓ ℋ has finite index in ℋ), we define a trace map from ModularForm (𝒢 ⊓ ℋ) k to ModularForm ℋ k.

instance instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup {ℋ : Subgroup (GL (Fin 2) ℝ)} : MulAction ↥ℋ ↥ℋ

Equations

• instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup = Monoid.toMulAction ↥ℋ

instance instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} : MulAction (↥ℋ) (↥ℋ ⧸ 𝒢.subgroupOf ℋ)

Equations

• instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf = MulAction.quotient (↥ℋ) (𝒢.subgroupOf ℋ)

def SlashInvariantForm.quotientFunc {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) (τ : UpperHalfPlane) : ℂ

For f invariant under 𝒢, this is a function on (ℋ ⧸ 𝒢 ⊓ ℋ) × ℍ → ℂ which packages up the translates of f by ℋ.

Equations

• SlashInvariantForm.quotientFunc f q τ = Quotient.liftOn q (fun (g : ↥ℋ) => SlashAction.map k (↑g)⁻¹ (⇑f) τ) ⋯

@[simp]

theorem SlashInvariantForm.quotientFunc_mk {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (h : ↥ℋ) : quotientFunc f ⟦h⟧ = SlashAction.map k (↑h)⁻¹ ⇑f

theorem SlashInvariantForm.quotientFunc_smul {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] {h : GL (Fin 2) ℝ} (hh : h ∈ ℋ) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : SlashAction.map k h (quotientFunc f q) = quotientFunc f (⟨h, hh⟩⁻¹ • q)

def SlashInvariantForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] [𝒢.IsFiniteRelIndex ℋ] : SlashInvariantForm ℋ k

The trace of a slash-invariant form, as a slash-invariant form.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SlashInvariantForm.coe_trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] [𝒢.IsFiniteRelIndex ℋ] : ⇑(SlashInvariantForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q

def SlashInvariantForm.norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] : SlashInvariantForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))

The norm of a slash-invariant form, as a slash-invariant form.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SlashInvariantForm.coe_norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] : ⇑(SlashInvariantForm.norm ℋ f) = ∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q

def ModularForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ModularFormClass F 𝒢 k] : ModularForm ℋ k

The trace of a modular form, as a modular form.

Equations

• ModularForm.trace ℋ f = { toSlashInvariantForm := SlashInvariantForm.trace ℋ f, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ModularFormClass F 𝒢 k] : ⇑(ModularForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, SlashInvariantForm.quotientFunc f q

def CuspForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [CuspFormClass F 𝒢 k] : CuspForm ℋ k

The trace of a cusp form, as a cusp form.

Equations

• CuspForm.trace ℋ f = { toSlashInvariantForm := (ModularForm.trace ℋ f).toSlashInvariantForm, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.coe_trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [CuspFormClass F 𝒢 k] : ⇑(CuspForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, SlashInvariantForm.quotientFunc f q

def ModularForm.norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] : ModularForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))

The norm of a modular form, as a modular form.

Equations

• ModularForm.norm ℋ f = { toSlashInvariantForm := SlashInvariantForm.norm ℋ f, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] : ⇑(ModularForm.norm ℋ f) = ∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, SlashInvariantForm.quotientFunc f q

theorem ModularForm.norm_ne_zero {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} {f : F} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] (hf : ⇑f ≠ 0) : ModularForm.norm ℋ f ≠ 0

theorem ModularForm.norm_eq_zero_iff {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] : ModularForm.norm ℋ f = 0 ↔ ⇑f = 0

theorem ModularForm.isZero_of_neg_weight {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} (hk : k < 0) (f : ModularForm 𝒢 k) : f = 0

theorem ModularForm.eq_const_of_weight_zero {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] (f : ModularForm 𝒢 0) : ∃ (c : ℂ), ⇑f = Function.const UpperHalfPlane c