Level-one parabolic cohomology vanishes in weights four through ten
ProvedMTT.Cohomology.parabolicH1_level_one_even_low_degreegroup-cohomologymodular-formsperiods
For n in {2,4,6,8}, the parabolic cohomology H¹_par(SL₂(ℤ), Symⁿ(ℂ²)) is zero, with the precise MTT left coefficient action and parabolic-cocycle quotient. These are the coefficient degrees corresponding to modular weights 4,6,8,10. This supplies additional level-one cases of the MTT parabolic cohomology dimension bound, independently of the analytic period isomorphism.
Preamble
import Definitions.Def_MTT_ParabolicCohomology set_option autoImplicit false noncomputable section
Formal statement
theorem MTT.Cohomology.parabolicH1_level_one_even_low_degree {n : ℕ}
(hn : Even n) (hnpos : 0 < n) (hnlt : n < 10) :
Subsingleton (MTT.Cohomology.ParabolicH1 1 n) := by sorrySource
An explicit finite-dimensional calculation of the two Manin relations, followed by the translation-normalized cocycle dimension bound proved in MTT.Cohomology.parabolicH1_add_one_le_periodRelations (88c8b791-3cba-42e8-bd56-b5e554f72d61). For the classical relation-space method, see 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 small-degree calculation here is supplied by explicit rational linear certificates, not assumed from the source.