Odd-weight parabolic cohomology comparison at level three

Proved

MTT.Cohomology.parabolicH1_finrank_le_level_three_odd

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

cohomologynumber-theory

For every odd integer $k\ge3$ , the degree- $k-2$ parabolic cohomology of $\Gamma_1(3)$ satisfies

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

This isolates level three after treating the level-four cohomological estimate by explicit generators. Its order-three elliptic contribution must be retained; the torsion-free large-level formula does not apply.

Preamble

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

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_level_three_odd {k : ℕ}
    (hk : 3 ≤ k) (hko : Odd k) :
    Module.finrank ℂ (ParabolicH1 3 (k - 2)) ≤
      2 * Module.finrank ℂ (CuspForm (MTT.GammaOne 3) (k : ℤ)) := by sorry

Source

Level-three specialization of MTT frontier c2c1a34b-7bfe-4fff-8533-9266b78c666a (Eichler-Shimura dimension comparison). Classical cusp dimensions: William Stein, Modular Forms: A Computational Approach, Chapter 6, Proposition 6.6, https://wstein.org/books/modform/modform/dimension_formulas.html .

View graph