MTT parabolic cohomology dimension bound at levels three and four

Proved

MTT.Cohomology.parabolicH1_finrank_le_levels_three_four

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

dimensiongroup-cohomologymtt

Let $N\in\{3,4\}$ and $k\ge3$ . Then

\dim_{\mathbb C}H^1_{\mathrm{par}}(\Gamma_1(N),\operatorname{Sym}^{k-2}\mathbb C^2)\le 2\dim_{\mathbb C}S_k(\Gamma_1(N)).

Here coefficients are homogeneous binary polynomials with the substitution action; parabolic cocycles restrict to principal cocycles on all rational-cusp stabilizers, and cohomology is taken modulo principal cocycles. This is the Eichler–Shimura dimension upper bound in the two remaining small levels, including odd weights. These levels require their actual elliptic and irregular-cusp corrections, not the torsion-free large-level dimension formula.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_levels_three_four {N k : ℕ}
    (hN : 3 ≤ N) (hN' : N ≤ 4) (hk : 3 ≤ k) :
    Module.finrank ℂ (MTT.Cohomology.ParabolicH1 N (k - 2)) ≤
      2 * Module.finrank ℂ (CuspForm (MTT.GammaOne N) (k : ℤ)) := by sorry

Source

Ash-Stevens, Modular forms in characteristic l and special values of their L-functions, Theorem 2.3, p. 853 (Eichler-Shimura for congruence subgroups), specialized to Gamma1(N), N=2,3,4, and the dimension upper-bound direction. Also Columbia Spring 2021 Eichler-Shimura notes, §1.2 Theorem 1, pp. 8-10: https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. Small-level corrections are recorded in Stein Chapter 6 Proposition 6.6: https://wstein.org/books/modform/modform/dimension_formulas.html.

View graph