Parabolic cohomology dimension bound for the Eichler–Shimura map

Proved

MTT.Cohomology.parabolicH1_finrank_le

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

group-cohomologymodular-formsperiods

Let $N>0$ and $k\ge 2$ . Write $S_k(\Gamma_1(N))$ for the complex vector space of holomorphic cusp forms and $V_{k-2}$ for homogeneous binary polynomials of degree $k-2$ with the left substitution action. Then

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

This is the dimension-comparison input in the Eichler–Shimura surjectivity argument. The coefficient module is the same as in the MTT period cocycle, and the parabolic condition is imposed at every rational cusp. Weight two and levels one and two are included. The statement contains no assumption that a period map is surjective.

Formalization Note Finite-dimensionality of the parabolic cohomology space is established separately. The inequality is stated using Lean's natural-number finite rank; the mathematical spaces here are finite-dimensional.

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 {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ 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, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf, §1.2, proof of Theorem 1, p. 9: equality of the two dimensions is the input before proving injectivity. This node isolates only the upper-bound half of that dimension equality, specialized to trivial coefficients apart from Sym^(k-2), and to Gamma1(N). It is an independent OPEN dimension-formula obligation, not an appeal to the parent surjectivity theorem.

View graph