Weight-one and weight-two modular seeds at level four

Proved

MTT.Cohomology.exists_weighted_modular_seeds_level_four

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

modular-formsnumber-theory

There are forms $A\in M_1(\Gamma_1(4))$ and $B\in M_2(\Gamma_1(4))$ whose expansions at infinity have orders

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

They can be chosen as $A(z)=\eta(2z)^{10}/(\eta(z)^4\eta(4z)^4)$ and $B(z)=\eta(4z)^8/\eta(2z)^4$ . Together with the nonzero weight-five cusp form, these supply the remaining level-four MTT dimension comparison.

Preamble

import Definitions.Def_MTT_Arithmetic
import Mathlib.NumberTheory.ModularForms.QExpansion

Formal statement

theorem MTT.Cohomology.exists_weighted_modular_seeds_level_four :
    ∃ A : ModularForm (MTT.GammaOne 4) 1,
      ∃ B : ModularForm (MTT.GammaOne 4) 2,
        MvPowerSeries.order (UpperHalfPlane.qExpansion 1 A) = 0 ∧
          MvPowerSeries.order (UpperHalfPlane.qExpansion 1 B) = 1 := by sorry

Source

Rouse–Webb, On spaces of modular forms spanned by eta-quotients, arXiv:1311.1460, pp. 1–2, https://arxiv.org/pdf/1311.1460 (theta and weight-two eta quotients). Modularity and cusp orders follow from Allen et al., arXiv:1901.10511, Theorems 1.2 and 1.4, pp. 2–3, https://arxiv.org/pdf/1901.10511 . Exponent vectors (-4,10,-4) and (0,-4,8) have cusp orders (0,1/2,0) and (0,0,1). The coprime-to-six corollary is not used.

View graph