A parabolic cohomology dimension bound from the two period relations

Proved

MTT.Cohomology.parabolicH1_add_one_le_periodRelations

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

group-cohomologymodular-formsperiods

Let $n>0$ be even, let $V_n=\operatorname{Sym}^n(\mathbf C^2)$ with the MTT left action $\rho$ , and put $R=ST$ for the standard matrices $S,T$ of $\mathrm{SL}_2(\mathbf Z)$ . For

W_n=\ker(1+\rho(S))\cap\ker(1+\rho(R)+\rho(R)^2),

one has

\dim_{\mathbf C}H^1_{\mathrm{par}}(\mathrm{SL}_2(\mathbf Z),V_n)+1\le\dim_{\mathbf C}W_n.

The additional one accounts for the nonzero principal-cocycle direction among translation-normalized cocycles. This is the algebraic reduction needed to compare level-one parabolic cohomology with the explicit period-polynomial dimension; it assumes no analytic Eichler–Shimura theorem.

Preamble

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

Formal statement

theorem MTT.Cohomology.parabolicH1_add_one_le_periodRelations {n : ℕ}
    (hn : Even n) (hnpos : 0 < n) :
    Module.finrank ℂ (MTT.Cohomology.ParabolicH1 1 n) + 1 ≤
      Module.finrank ℂ (MTT.Cohomology.periodRelations n) := by sorry

Source

Don Zagier, Periods of modular forms, traces of Hecke operators, and multiple zeta values, RIMS Kokyuroku 843 (1993), pp. 162–164, https://people.mpim-bonn.mpg.de/zagier/files/kokyuroku/843/fulltext.pdf. The source identifies translation-normalized cocycles with period relations and the residual principal direction. This node proves only the necessary dimension inequality, directly from normalization, S,T generation, the torsion relations S^2=(ST)^3=-I, and a nonzero principal cocycle. The MTT left action is retained throughout; the analytic period isomorphism is not used.

View graph