Degree-zero parabolic cohomology vanishes at level one

Proved

MTT.Cohomology.parabolicH1_level_one_degree_zero

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

group-cohomologymodular-formsperiods

The first parabolic cohomology of $\mathrm{SL}_2(\mathbf Z)=\Gamma_1(1)$ with constant complex coefficients is zero:

H^1_{\mathrm{par}}(\mathrm{SL}_2(\mathbf Z),\mathbf C)=0.

Here the coefficient module is the degree-zero homogeneous binary-polynomial space, with its trivial MTT action. This settles the level-one, weight-two case of the dimension bound used for Eichler–Shimura surjectivity.

Formalization Note Vanishing means that the parabolic cocycle quotient is a subsingleton.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.Cohomology.parabolicH1_level_one_degree_zero :
    Subsingleton (MTT.Cohomology.ParabolicH1 1 0) := by sorry

Source

Elementary calculation using the standard generators S,T of SL2(Z), the relation S^4=1 and the parabolic restriction at infinity. The generators theorem is SpecialLinearGroup.SL2Z_generators in mathlib's Mathlib.LinearAlgebra.Matrix.FixedDetMatrices. This independently proves the N=1, k=2 case of MTT.Cohomology.parabolicH1_finrank_le (14a60394-65be-4ad3-9c28-3252b43a5d06); no Eichler–Shimura theorem is assumed.

View graph