Even-weight parabolic cohomology bound at levels three and four

Proved

MTT.Cohomology.parabolicH1_finrank_le_levels_three_four_even

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

cohomologynumber-theory

For $N\in\{3,4\}$ and an even weight $k\ge3$ , the parabolic cohomology of $\Gamma_1(N)$ with degree- $k-2$ binary-form coefficients has complex dimension at most twice the dimension of $S_k(\Gamma_1(N))$ . Parabolic cocycles restrict to principal cocycles on every rational cusp stabilizer, and cohomology is taken modulo principal cocycles. This is the even-weight part of the remaining small-level dimension input in the MTT mission.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_levels_three_four_even {N k : ℕ}
    (hN : 3 ≤ N) (hN' : N ≤ 4) (hk : 3 ≤ k) (hke : Even k) :
    Module.finrank ℂ (ParabolicH1 N (k - 2)) ≤
      2 * Module.finrank ℂ (CuspForm (MTT.GammaOne N) (k : ℤ)) := by sorry

Source

Eichler-Shimura dimension comparison; at N=3,4, adjoining -I to Gamma1(N) gives Gamma0(N), and the center acts trivially in even symmetric degree. Supporting case of MTT frontier 36b8715f-dd40-4647-a91c-af4224ece24c.

View graph