Translation normalization adds one dimension to parabolic cohomology

Proved

MTT.Cohomology.normalizedParabolic_finrank

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

group-cohomologymodular-formsperiods

Let $N,n>0$ , let $V_n=\operatorname{Sym}^n(\mathbf C^2)$ carry the MTT left action of $\Gamma_1(N)$ , and let $T=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ . Write $Z^1_{\mathrm{par},T}$ for the space of parabolic cocycles $c$ with $c(T)=0$ . Then

\dim_{\mathbf C} Z^1_{\mathrm{par},T}(\Gamma_1(N),V_n)=\dim_{\mathbf C}H^1_{\mathrm{par}}(\Gamma_1(N),V_n)+1.

Thus translation normalization leaves precisely one dimension of principal cocycles, uniformly in the positive level and degree. This supplies the exact algebraic normalization correction for the general-level dimension branch of the MTT mission; no parity assumption or period-map theorem is required.

Preamble

import Definitions.Def_MTT_NormalizedParabolicCocycles
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.Cohomology.normalizedParabolic_finrank {N n : ℕ} (hN : 0 < N) (hn : 0 < n) :
    Module.finrank ℂ (MTT.Cohomology.normalizedParabolic N n) =
      Module.finrank ℂ (MTT.Cohomology.ParabolicH1 N n) + 1 := by sorry

Source

Parabolic cocycle normalization at infinity, in the standard group-cohomology realization described in Columbia Spring 2021 Eichler-Shimura seminar notes, section 1.1, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. The proof explicitly identifies the normalization kernel with the principal cocycle of X^n. Its T-invariant polynomial lemma adapts accepted MTT proof 2c3fe658-d2de-4575-89b3-ebdfcfd22e7e, with the attribution retained in the solution.

View graph