Weight-two cusp forms on Γ₀(2)

DefinitionNorm of a cusp form#✓fully proved

The product norm of a cusp form: for 𝒢 of finite relative index in ℋ, the product of the ℋ / 𝒢-translates of f, viewed as a cusp form on the larger group ℋ at weight k * [ℋ : 𝒢]. This lifts Mathlib's ModularForm.norm to cusp forms; the only new work is checking vanishing at the cusps, which follows because each translate is a cusp form.

CuspForm.norm · 19 lines

noncomputable def norm {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type*} [FunLike F ℍ ℂ]
    {k : ℤ} [CuspFormClass F 𝒢 k] (ℋ : Subgroup (GL (Fin 2) ℝ))
    [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] (f : F) :
    CuspForm ℋ (k * Nat.card (ℋ ⧸ 𝒢.subgroupOf ℋ)) where
  __ := ModularForm.norm ℋ f
  zero_at_cusps' h γ := by
    rintro rfl
    simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_norm, IsZeroAtImInfty,
      Filter.ZeroAtFilter]
    let := Fintype.ofFinite (ℋ ⧸ 𝒢.subgroupOf ℋ)
    rw [Nat.card_eq_fintype_card, ← Finset.card_univ, ModularForm.prod_slash]
    refine Filter.ZeroAtFilter.smul _ ?_
    change Filter.Tendsto _ _ (nhds 0)
    rw [show (0 : ℂ) = ∏ _q : ℋ ⧸ 𝒢.subgroupOf ℋ, (0 : ℂ) by
        rw [Finset.prod_const, Finset.card_univ, zero_pow Fintype.card_ne_zero],
      Finset.prod_fn]
    refine tendsto_finsetProd _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)
    refine (CuspForm.translate f _).zero_at_cusps' ?_ γ rfl
    simpa using h.of_isFiniteRelIndex_conj hr

Used by 3

Used byCusp form norm agrees with the modular form norm · Norm of a cusp form vanishes only for the zero form · No nonzero weight-two cusp forms on Γ₀(2)

LemmaCusp form norm agrees with the modular form norm#✓fully proved

The coercion of the norm of a cusp form is the norm of its coercion as a modular form.

lemma coe_norm_eq_coe_modularFormNorm {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type*}
    [FunLike F ℍ ℂ] {k : ℤ} [CuspFormClass F 𝒢 k] (ℋ : Subgroup (GL (Fin 2) ℝ))
    [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] (f : F) :
    (CuspForm.norm ℋ f : ℍ → ℂ) = (ModularForm.norm ℋ f : ℍ → ℂ)

Uses 1 · Used by 1

Statement usesNorm of a cusp form

Used byNorm of a cusp form vanishes only for the zero form

LemmaNorm of a cusp form vanishes only for the zero form#✓fully proved

The norm of a cusp form vanishes if and only if the form itself vanishes: the norm is a product of translates, and a translate of a nonzero form is nonzero.

lemma norm_eq_zero_iff {𝒢 : Subgroup (GL (Fin 2) ℝ)} {F : Type*} [FunLike F ℍ ℂ]
    {k : ℤ} [CuspFormClass F 𝒢 k] (ℋ : Subgroup (GL (Fin 2) ℝ))
    [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] (f : F) :
    CuspForm.norm ℋ f = 0 ↔ (f : ℍ → ℂ) = 0

Uses 2 · Used by 1

Statement usesNorm of a cusp form

Proof usesCusp form norm agrees with the modular form norm

Used byNo nonzero weight-two cusp forms on Γ₀(2)

TheoremΓ₀(2) has index 3 in SL(2, ℤ)#✓fully proved

The index of Γ₀(2) in SL(2, ℤ) is 3: the cosets are classified by the first column mod 2, and there are three nonzero vectors in (ZMod 2)².

theorem Gamma0_two_index_eq_three : (Gamma0 2).index = 3

Used by 1

Used byNo nonzero weight-two cusp forms on Γ₀(2)

TheoremNo nonzero weight-two cusp forms of level one#✓fully proved

Every weight-two cusp form on Γ₀(1) is zero: Γ₀(1) is the full modular group, and the dimension formula gives rank zero below weight 12.

theorem S2_Gamma0_one_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 1) 2) :
    f = 0

TheoremNo nonzero weight-two cusp forms on Γ₀(2)#✓fully proved

Every weight-two cusp form on Γ₀(2) is zero. Take the norm of f to Γ₀(1): it has weight 2 * [Γ₀(1) : Γ₀(2)] = 6, hence vanishes by the level-one dimension formula, and the norm vanishes only when f does.

theorem S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) :
    f = 0

Uses 3

Proof usesΓ₀(2) has index 3 in SL(2, ℤ) · Norm of a cusp form · Norm of a cusp form vanishes only for the zero form

TheoremNorm trick for modular forms#✓fully proved

The norm trick: two modular forms satisfying a commutation relation under the slash action of ℋ give rise to a modular form Φ of level ℋ with Φ * G = F * norm ℋ G.

theorem exists_mul_eq_mul_norm_of_forall_slash_mul_eq
    (𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] {k : ℤ}
    (F G : ModularForm 𝒢 k)
    (hFG : ∀ h ∈ ℋ, ((⇑F : UpperHalfPlane → ℂ) ∣[k] h) * (⇑G : UpperHalfPlane → ℂ) =
      (⇑F : UpperHalfPlane → ℂ) * ((⇑G : UpperHalfPlane → ℂ) ∣[k] h)) :
    ∃ Φ : ModularForm ℋ (k * Nat.card (ℋ ⧸ 𝒢.subgroupOf ℋ)),
      (⇑Φ : UpperHalfPlane → ℂ) * (⇑G : UpperHalfPlane → ℂ) =
        (⇑F : UpperHalfPlane → ℂ) * (⇑(ModularForm.norm ℋ G) : UpperHalfPlane → ℂ)

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.