The MTT parabolic dimension bound in weight two at every positive level
ProvedMTT.Cohomology.parabolicH1_finrank_le_weight_twogroup-cohomologymodular-formsperiods
For every positive integer N, the complex dimension of the first parabolic cohomology of Gamma_1(N) with degree-zero homogeneous-polynomial coefficients is at most twice the dimension of its weight-two cusp forms. This is the full weight-two case of the MTT mission's general dimension frontier. Degree-zero polynomials are constant, so the proof compares the MTT cocycles with scalar-valued parabolic characters. It includes all small levels and uses no period-map injectivity assumption.
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_weight_two {N : ℕ} (hN : 0 < N) :
Module.finrank ℂ (MTT.Cohomology.ParabolicH1 N 0) ≤
2 * Module.finrank ℂ (CuspForm (MTT.GammaOne N) 2) := by sorrySource
Columbia Spring 2021 Eichler-Shimura seminar notes, Section 1.2, Theorem 1 and its dimension comparison, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. The proof reuses the already-proved platform theorems ModularCurve.Period.exists_basis_parabolicHoms_of_isAddTorsionFree (4b95a52a-d74a-57d1-ba7d-5f43023fa729) and ModularCurve.finrank_parabolicHoms_le_two_mul_finrank_cuspForm_of_isCongruenceSubgroup (0ecd14cb-bbeb-5b1a-98cb-394f76c9069f), originating in the FLT repository at commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef. The MTT-to-scalar comparison is proved explicitly in the submission.