Parabolic Shapiro dimension comparison with central-fixed coinduction

Proved

MTT.Cohomology.parabolicH1_finrank_le_centralCoinduced

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

group-cohomologymttshapiro

Let $N>0$ , $n\ge0$ , $H=\Gamma_1(N)$ , $G=\mathrm{SL}_2(\mathbb Z)$ , and $V=\operatorname{Sym}^n\mathbb C^2$ with the MTT substitution action. Let $W=\operatorname{Coind}_H^G V$ and let $W^+$ be the subrepresentation fixed by $-I$ . Then

\dim_{\mathbb C}H^1_{\mathrm{par}}(H,V)\le \dim_{\mathbb C}H^1_{\mathrm{par}}(G,W^+).

In both spaces, parabolic means principal upon restriction to each rational-cusp stabilizer. This comparison is the parabolic Shapiro dimension inequality after removing the nontrivial central summand. It applies in every degree, with no parity assumption, and permits subsequent full-group estimates on a representation with trivial central action.

Preamble

import Definitions.Def_MTT_FullParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

theorem MTT.Cohomology.parabolicH1_finrank_le_centralCoinduced {N n : ℕ} (hN : 0 < N) :
    Module.finrank ℂ (MTT.Cohomology.ParabolicH1 N n) ≤
      Module.finrank ℂ (MTT.Cohomology.FullParabolicH1
        (MTT.Cohomology.centralCoinduced N n)) := by sorry

Source

Columbia Spring 2021 Eichler-Shimura notes, section 1.1 Lemma 1 (parabolic Shapiro), https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. Parabolic lifting is already proved as platform theorem 96bbed5a-210d-4d60-8934-d83a912e2875. The central-fixed refinement is an explicit algebraic consequence, not a literal quotation: for z=-I the cocycle identity gives ((id+rho(z))/2)c(g)-c(g)=(rho(g)-id)c(z)/2. The submitted proof checks this refinement and parabolic compatibility directly.

View graph