MTT parabolic dimension bound at levels two, three and four

Proved

MTT.Cohomology.parabolicH1_finrank_le_levels_two_three_four

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

dimensiongroup-cohomologymtt

Let $N\in\{2,3,4\}$ and let $k\ge3$ be a natural number. Then

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

This isolates the exceptional small levels, where elliptic or irregular-cusp corrections prevent using the uncorrected N>=5 dimension formula. The assertion remains OPEN and covers odd as well as even weights.

Preamble

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

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_levels_two_three_four {N k : ℕ}
    (hN : 2 ≤ 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