MTT parabolic cohomology dimension bound at level two

Proved

MTT.Cohomology.parabolicH1_finrank_le_level_two

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

group-cohomologymodular-formsmtt

For every integer weight $k\ge2$ , the complex dimension of the parabolic first cohomology of $\Gamma_1(2)$ with coefficients in homogeneous binary polynomials of degree $k-2$ is at most twice the dimension of its weight- $k$ cusp forms:

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

The parabolic condition means that the cocycle restricts to a principal cocycle on every rational-cusp stabilizer; the cohomology is the quotient by principal cocycles. This is the level-two dimension upper-bound direction of Eichler–Shimura, in the MTT coefficient convention. It includes both even and odd weights.

Preamble

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

Formal statement

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

Source

Ash-Stevens, Modular forms in characteristic l and special values of their L-functions, Theorem 2.3, p. 853, specialized to Gamma1(2)=Gamma0(2). Existing platform Gamma0 decomposition: theorem 4c20e75e-94cc-59a9-a6e0-3792a09ffb66 (HeckeEis.exists_eichlerShimura_coeffH1par_binaryFormRepSL). Group equality also in Stein, Modular Forms, Chapter 6, dimension formulas for Gamma1(N), https://wstein.org/books/modform/modform/dimension_formulas.html.

View graph