Low-weight modular and cusp-form seeds at level three

Proved

MTT.Cohomology.exists_weighted_cusp_seeds_level_three

by cbirkbeck · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

There exist forms $A\in M_1(\Gamma_1(3))$ , $B\in M_3(\Gamma_1(3))$ and a nonzero cusp form $D\in S_6(\Gamma_1(3))$ such that their q-expansions at infinity satisfy

\operatorname{ord}_q(A)=0,\qquad\operatorname{ord}_q(B)=1.

One choice is the normalized weight-one Eisenstein series for the quadratic character of discriminant $-3$ , together with $B(z)=\eta(3z)^9/\eta(z)^3$ and $D(z)=\eta(z)^6\eta(3z)^6$ . Their weighted monomials supply the MTT level-three cusp-form dimension lower bound.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.NumberTheory.ModularForms.QExpansion
open UpperHalfPlane

Formal statement

theorem MTT.Cohomology.exists_weighted_cusp_seeds_level_three :
    ∃ A : ModularForm (MTT.GammaOne 3) 1,
      ∃ B : ModularForm (MTT.GammaOne 3) 3,
        ∃ D : CuspForm (MTT.GammaOne 3) 6,
          (qExpansion 1 A).order = 0 ∧ (qExpansion 1 B).order = 1 ∧ D ≠ 0 := by sorry

Source

Explicit specialization of the sufficient eta-quotient modularity criterion and cusp-order formula, Allen–Anderson–Hamakiotes–Oltsik–Swisher, Eta-quotients of Prime or Semiprime Level and Elliptic Curves, arXiv:1901.10511, Theorems 1.2 and 1.4, pp. 2–3, https://arxiv.org/pdf/1901.10511 . These two results apply to arbitrary N; the coprime-to-6 Corollary 1.8 is not used. The weight-one input is the existing proved EisensteinWeightOne.e1Chi3IsModular, b77f5563-c246-5dea-ac05-9934aeb4fd42, with constant term 1.

View graph