The remaining MTT dimension comparison at higher level and positive coefficient degree

Proved

MTT.Cohomology.parabolicH1_finrank_le_higher_level_weight

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

group-cohomologymodular-formsperiods

Let $N\ge2$ and $k\ge3$ be integers. For the usual left action on homogeneous binary polynomials, the parabolic cohomology of $\Gamma_1(N)$ satisfies

\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)).

This is the part of the MTT mission's dimension comparison left after the level-one and weight-two cases have been proved separately. No parity or torsion-free assumption is imposed. The statement is a dimension bound, independent of the construction or injectivity of the period map.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
set_option autoImplicit false
noncomputable section

Formal statement

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

Source

Columbia Spring 2021 Eichler-Shimura seminar notes, Section 1.2, proof of Theorem 1, page 9: the equality of dimensions used for Eichler-Shimura, specialized here to its upper-bound direction and N >= 2, k >= 3. https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. This is an explicitly open residual case, not a claim that Riemann-Roch or a finite-dimensionality argument has already been formalized.

View graph