Vanishing of odd symmetric-power parabolic cohomology at levels one and two

Proved

MTT.Cohomology.parabolicH1_subsingleton_of_odd_small_level

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

group-cohomologymodular-formsperiods

Let $N\in\{1,2\}$ and let $n\ge 0$ be odd. For the MTT left action on homogeneous binary polynomials $V_n=\operatorname{Sym}^n(\mathbf C^2)$ , the parabolic cohomology vanishes:

H^1_{\mathrm{par}}(\Gamma_1(N),V_n)=0.

This isolates the small-level odd-weight cases of the cohomological dimension comparison used for Eichler–Shimura surjectivity. In weight $k=n+2$ , it implies the required upper bound on parabolic cohomology without any dimension formula for cusp forms.

Formalization Note Vanishing is expressed by the quotient vector space being a subsingleton.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.Cohomology.parabolicH1_subsingleton_of_odd_small_level {N n : ℕ}
    (hN : 0 < N) (hN₂ : N ≤ 2) (hn : Odd n) :
    Subsingleton (MTT.Cohomology.ParabolicH1 N n) := by sorry

Source

Elementary central-element argument: -I is central in Gamma1(N) for N=1,2 and acts by (-1)^n on Sym^n. The proof will explicitly express every one-cocycle as a principal cocycle. This is a supporting lemma for MTT.Cohomology.parabolicH1_finrank_le (14a60394-65be-4ad3-9c28-3252b43a5d06), independent of period injectivity or surjectivity. The parabolic quotient is that of Columbia Spring 2021 Eichler–Shimura notes §1.1, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf.

View graph