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

Proved

MTT.Cohomology.exists_weighted_cusp_seeds_level_four

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

modular-formsnumber-theory

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

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

One choice is $A(z)=\eta(2z)^{10}/(\eta(z)^4\eta(4z)^4)$ , $B(z)=\eta(4z)^8/\eta(2z)^4$ , and $D(z)=\eta(z)^4\eta(2z)^2\eta(4z)^4$ . Their weighted monomials supply the MTT odd-weight level-four cusp-form dimension lower bound. The odd-weight forms are asserted on $\Gamma_1(4)$ , not with trivial character on $\Gamma_0(4)$ .

Preamble

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

Formal statement

theorem MTT.Cohomology.exists_weighted_cusp_seeds_level_four :
    ∃ A : ModularForm (MTT.GammaOne 4) 1,
      ∃ B : ModularForm (MTT.GammaOne 4) 2,
        ∃ D : CuspForm (MTT.GammaOne 4) 5,
          (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 theta and weight-two eta quotients are also displayed in Rouse–Webb, On spaces of modular forms spanned by eta-quotients, arXiv:1311.1460, pp. 1–2, https://arxiv.org/pdf/1311.1460 .

View graph