Central-fixed coinduced cohomology bounded by three fixed subspaces

Proved

MTT.Cohomology.centralCoinduced_parabolicH1_add_fixed_finrank_le

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

dimensiongroup-cohomologymtt

For integers $N,n>0$ , let $W^+$ be the $-I$ -fixed subrepresentation of the coinduction of $\operatorname{Sym}^n\mathbb C^2$ from $\Gamma_1(N)$ to $G=\mathrm{SL}_2(\mathbb Z)$ . Write $(W^+)^g=\ker(\rho(g)-1)$ . With the standard modular generators $S,T$ , one has

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

Parabolic means principal on every rational-cusp stabilizer. This is the full-group cohomological estimate before evaluating the finite-coset fixed-space dimensions. There is no parity condition on $n$ and no large-level restriction on $N$ .

Preamble

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

Formal statement

theorem MTT.Cohomology.centralCoinduced_parabolicH1_add_fixed_finrank_le {N n : ℕ} (hN : 0 < N) (hn : 0 < n) :
    Module.finrank ℂ (MTT.Cohomology.FullParabolicH1 (MTT.Cohomology.centralCoinduced N n)) +
        Module.finrank ℂ ((MTT.Cohomology.centralCoinduced N n).ρ
          ModularGroup.S - LinearMap.id).ker +
        Module.finrank ℂ ((MTT.Cohomology.centralCoinduced N n).ρ
          (ModularGroup.S * ModularGroup.T) - LinearMap.id).ker +
        Module.finrank ℂ ((MTT.Cohomology.centralCoinduced N n).ρ
          ModularGroup.T - LinearMap.id).ker ≤
      Module.finrank ℂ (MTT.Cohomology.centralCoinduced N n) := by sorry

Source

Specialization of the proved platform theorem HeckeEis.finrank_coeffH1par_top_add_le, 09d43972-ece9-52d3-bf78-53cfcb5e7dc8, proof 681a125a-6dca-5d6b-8fc1-b096b029b391, to the central-fixed coinduced coefficient module. All central-action, invariant, coinvariant and coefficient-model comparison hypotheses are discharged in the submission. The three-generator relation calculation implements the cohomological dimension argument in Columbia Spring 2021 Eichler-Shimura notes, section 1.2, Theorem 1, pp. 8-10, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf.

View graph