Restriction, translation, norm and trace

This file defines operations on modular forms, cusp forms, and slash-invariant forms which change the level:

• restriction maps (making the level group smaller, without changing the underlying function)
• translation maps (acting by a slash operator on the underlying function, and conjugating the level group)
• trace and norm maps (making the level group larger, by taking a sum / product of translates by coset representatives).

As an application, we show that a modular form of weight ≤ 0 (and any level) must be constant, using norm maps to reduce to the case of level SL(2, ℤ).

noncomputable def SlashInvariantForm.translate {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [SlashInvariantFormClass F 𝒢 k] : 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 {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [SlashInvariantFormClass F 𝒢 k] : ⇑(translate f g) = SlashAction.map k g ⇑f

noncomputable def ModularForm.translate {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [ModularFormClass F 𝒢 k] : ModularForm (ConjAct.toConjAct g⁻¹ • 𝒢) k

Translating a ModularForm by GL(2, ℝ), to obtain a new ModularForm.

Equations

• ModularForm.translate f g = { toSlashInvariantForm := SlashInvariantForm.translate f g, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_translate {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [ModularFormClass F 𝒢 k] : ⇑(translate f g) = SlashAction.map k g ⇑f

noncomputable def CuspForm.translate {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [CuspFormClass F 𝒢 k] : CuspForm (ConjAct.toConjAct g⁻¹ • 𝒢) k

Translating a CuspForm by SL(2, ℤ), to obtain a new CuspForm.

Equations

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

@[simp]

theorem CuspForm.coe_translate {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) (g : GL (Fin 2) ℝ) [CuspFormClass F 𝒢 k] : ⇑(translate f g) = SlashAction.map k g ⇑f

def SlashInvariantForm.restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : SlashInvariantForm ℋ k) : SlashInvariantForm 𝒢 k

Regard a modular form as a form for a subgroup of its level.

Equations

• SlashInvariantForm.restrict hGH f = { toFun := ⇑f, slash_action_eq' := ⋯ }

@[simp]

theorem SlashInvariantForm.coe_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : SlashInvariantForm ℋ k) : ⇑(restrict hGH f) = ⇑f

theorem SlashInvariantForm.restrict_injective {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) : Function.Injective (restrict hGH)

@[simp]

theorem SlashInvariantForm.restrict_eq_zero_iff {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : SlashInvariantForm ℋ k} : restrict hGH f = 0 ↔ f = 0

@[simp]

theorem SlashInvariantForm.restrict_translate {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : SlashInvariantForm ℋ k} (g : GL (Fin 2) ℝ) : restrict ⋯ (translate f g) = translate (restrict hGH f) g

def ModularForm.restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : ModularForm ℋ k) : ModularForm 𝒢 k

Regard a modular form as a form for a subgroup of its level.

Equations

• ModularForm.restrict hGH f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : ModularForm ℋ k) : ⇑(restrict hGH f) = ⇑f

theorem ModularForm.restrict_injective {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) : Function.Injective (restrict hGH)

@[simp]

theorem ModularForm.restrict_eq_zero_iff {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : ModularForm ℋ k} : restrict hGH f = 0 ↔ f = 0

@[simp]

theorem ModularForm.restrict_translate {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : ModularForm ℋ k} (g : GL (Fin 2) ℝ) : restrict ⋯ (translate f g) = translate (restrict hGH f) g

def ModularForm.restrictₗ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} (k : ℤ) (R : Type u_2) [Semiring R] [SMul R ℂ] [Module R (ModularForm 𝒢 k)] [Module R (ModularForm ℋ k)] [IsSMulApply R (ModularForm 𝒢 k) UpperHalfPlane ℂ] [IsSMulApply R (ModularForm ℋ k) UpperHalfPlane ℂ] (hGH : 𝒢 ≤ ℋ) : ModularForm ℋ k →ₗ[R] ModularForm 𝒢 k

Restriction bundled as a linear map. The typeclass assumptions will be satisfied for R = ℝ and any levels, or R = ℂ if HasDetOne is available.

Equations

• ModularForm.restrictₗ k R hGH = { toFun := ModularForm.restrict hGH, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModularForm.restrictₗ_apply {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} (k : ℤ) (R : Type u_2) [Semiring R] [SMul R ℂ] [Module R (ModularForm 𝒢 k)] [Module R (ModularForm ℋ k)] [IsSMulApply R (ModularForm 𝒢 k) UpperHalfPlane ℂ] [IsSMulApply R (ModularForm ℋ k) UpperHalfPlane ℂ] (hGH : 𝒢 ≤ ℋ) : ⇑(restrictₗ k R hGH) = restrict hGH

theorem ModularForm.restrictₗ_injective {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} (k : ℤ) (R : Type u_2) [Semiring R] [SMul R ℂ] [Module R (ModularForm 𝒢 k)] [Module R (ModularForm ℋ k)] [IsSMulApply R (ModularForm 𝒢 k) UpperHalfPlane ℂ] [IsSMulApply R (ModularForm ℋ k) UpperHalfPlane ℂ] (hGH : 𝒢 ≤ ℋ) : Function.Injective ⇑(restrictₗ k R hGH)

def CuspForm.restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : CuspForm ℋ k) : CuspForm 𝒢 k

Regard a cusp form as a form for a subgroup of its level.

Equations

• CuspForm.restrict hGH f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.coe_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) (f : CuspForm ℋ k) : ⇑(restrict hGH f) = ⇑f

theorem CuspForm.restrict_injective {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) : Function.Injective (restrict hGH)

@[simp]

theorem CuspForm.restrict_eq_zero_iff {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : CuspForm ℋ k} : restrict hGH f = 0 ↔ f = 0

@[simp]

theorem CuspForm.restrict_translate {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hGH : 𝒢 ≤ ℋ) {f : CuspForm ℋ k} (g : GL (Fin 2) ℝ) : restrict ⋯ (translate f g) = translate (restrict hGH f) g

@[instance_reducible]

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

Equations

• instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup = Monoid.toMulAction ↥ℋ

@[instance_reducible]

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

Equations

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

noncomputable def SlashInvariantForm.quotientFunc {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) (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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) (h : ↥ℋ) : quotientFunc f ⟦h⟧ = SlashAction.map k (↑h)⁻¹ ⇑f

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

noncomputable def SlashInvariantForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) [𝒢.IsFiniteRelIndex ℋ] : ⇑(SlashInvariantForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q

noncomputable def SlashInvariantForm.norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] (f : F) [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] : ⇑(SlashInvariantForm.norm ℋ f) = ∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q

noncomputable def ModularForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.IsFiniteRelIndex ℋ] [ModularFormClass F 𝒢 k] : ⇑(ModularForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, SlashInvariantForm.quotientFunc f q

noncomputable def CuspForm.trace {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.IsFiniteRelIndex ℋ] [CuspFormClass F 𝒢 k] : ⇑(CuspForm.trace ℋ f) = ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, SlashInvariantForm.quotientFunc f q

noncomputable def ModularForm.norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {f : F} [𝒢.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} [FunLike F UpperHalfPlane ℂ] {k : ℤ} (f : F) [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] : ModularForm.norm ℋ f = 0 ↔ ⇑f = 0

theorem quotientFunc_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm ℋ k) (hGH : 𝒢 ≤ ℋ) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : SlashInvariantForm.quotientFunc (ModularForm.restrict hGH f) q = ⇑f

theorem trace_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] (f : ModularForm ℋ k) (hGH : 𝒢 ≤ ℋ) : ModularForm.trace ℋ (ModularForm.restrict hGH f) = 𝒢.relIndex ℋ • f

Composite of trace and restriction maps.

theorem norm_restrict {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] (f : ModularForm ℋ k) (hGH : 𝒢 ≤ ℋ) [ℋ.HasDetPlusMinusOne] : ⇑(ModularForm.norm ℋ (ModularForm.restrict hGH f)) = ⇑f ^ 𝒢.relIndex ℋ

Composite of norm and restriction maps. Formulated as an equality after coercing to functions, to avoid issues with type equality.

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