Finite-dimensional parabolic cohomology for Gamma1(N)

Proved

MTT.Cohomology.parabolicH1_finiteDimensional

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

group-cohomologymodular-formsperiods

Let $N$ be a positive integer and $n\ge 0$ . Let $V_n$ be the complex space of homogeneous binary polynomials of degree $n$ , with the MTT left substitution action of $\Gamma_1(N)$ . Then

\dim_{\mathbf C} H^1_{\mathrm{par}}(\Gamma_1(N),V_n)<\infty.

Here parabolic cohomology is formed from the ordinary one-cocycles whose restriction to each cyclic cusp stabilizer is principal, modulo all principal coboundaries. This is the finiteness input needed to use dimension comparisons in the Eichler–Shimura surjectivity argument; it includes $n=0$ and all positive levels.

Preamble

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

Formal statement

theorem MTT.Cohomology.parabolicH1_finiteDimensional {N n : ℕ} (hN : 0 < N) :
    FiniteDimensional ℂ (MTT.Cohomology.ParabolicH1 N n) := by sorry

Source

Columbia Spring 2021 Eichler–Shimura seminar notes, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf, §1.1 pp. 1–3 (cocycles, coboundaries, parabolic restriction, finite cellular model), §1.2 Theorem 1 p. 9. The submitted direct proof instead uses finite generation: mathlib SpecialLinearGroup.SL2Z_generators (Mathlib.LinearAlgebra.Matrix.FixedDetMatrices), Subgroup.fg_of_index_ne_zero (Mathlib.GroupTheory.Schreier), and MvPolynomial.homogeneousSubmodule_fg.

View graph