The parabolic cohomology dimension bound for all level-one weights
ProvedMTT.Cohomology.parabolicH1_finrank_le_level_onegroup-cohomologymodular-formsperiods
For every integer weight k >= 2, the complex dimension of the parabolic first cohomology of SL_2(Z) with coefficients in Sym^(k-2)(C^2), using the MTT left coefficient action, is at most twice the complex dimension of the level-one cusp forms of weight k. This is the complete N=1 case of the MTT mission's open theorem MTT.Cohomology.parabolicH1_finrank_le. The proof includes weight two and odd weights; it does not assume period-map injectivity or Eichler-Shimura surjectivity.
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_level_one {k : ℕ} (hk : 2 ≤ k) :
Module.finrank ℂ (MTT.Cohomology.ParabolicH1 1 (k - 2)) ≤
2 * Module.finrank ℂ (CuspForm (MTT.GammaOne 1) (k : ℤ)) := by sorrySource
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 proof combines a direct cocycle/coinvariant argument and explicit elliptic fixed-space counts with mathlib's proved level-one modular-form dimension formula. See the submitted proof explanation for the action convention and attribution of the translation-invariant polynomial argument.