Large-level parabolic dimension count for central-fixed coinduced coefficients

Proved

MTT.Cohomology.centralCoinduced_parabolicH1_dimension_upper_bound

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

dimensiongroup-cohomologymtt

Let $N\ge5$ and $k\ge3$ . Put $G=\mathrm{SL}_2(\mathbb Z)$ , $H=\Gamma_1(N)$ , $V=\operatorname{Sym}^{k-2}\mathbb C^2$ , and $W^+=(\operatorname{Coind}_H^G V)^{-I=1}$ . Let $\mu=[G:\langle H,-I\rangle]$ and $c=\#(H\backslash G/\langle T,-I\rangle)$ , where $T=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ . Then

6\dim_{\mathbb C}H^1_{\mathrm{par}}(G,W^+)+6c\le(k-1)\mu.

The parabolic condition uses all rational-cusp stabilizers. This is the independent cohomological dimension count on the full modular group, with the central action already made trivial. Together with the parabolic Shapiro comparison, it gives the MTT large-level upper bound. The restrictions $N\ge5$ exclude the small-level elliptic and irregular-cusp corrections.

Preamble

import Definitions.Def_MTT_FullParabolicCohomology
import Mathlib.GroupTheory.DoubleCoset
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
open scoped MatrixGroups

Formal statement

theorem MTT.Cohomology.centralCoinduced_parabolicH1_dimension_upper_bound {N k : ℕ}
    (hN : 5 ≤ N) (hk : 3 ≤ k) :
    6 * Module.finrank ℂ (MTT.Cohomology.FullParabolicH1 (MTT.Cohomology.centralCoinduced N (k - 2))) +
        6 * Nat.card (DoubleCoset.Quotient (CongruenceSubgroup.Gamma1 N : Set SL(2, ℤ))
          ((Subgroup.zpowers ModularGroup.T ⊔ Subgroup.zpowers (-1) : Subgroup SL(2, ℤ)) :
            Set SL(2, ℤ))) ≤
      (k - 1) * (CongruenceSubgroup.Gamma1 N ⊔ Subgroup.zpowers (-1 : SL(2, ℤ))).index := by sorry

Source

Columbia Spring 2021 Eichler-Shimura notes, §1.1 Lemma 1 and §1.2 Theorem 1, pp. 8-10: https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. This is the cohomological upper-bound direction of that dimension comparison, with the N>=5 index/cusp expression from Stein, Modular Forms: A Computational Approach, Chapter 6, Proposition 6.6 and preceding genus formula: https://wstein.org/books/modform/modform/dimension_formulas.html. It is a source-faithful consequence, not a literal quoted statement; its independent algebraic proof remains open. Here the parabolic Shapiro isomorphism and central-involution averaging transport the same dimension formula to the central-fixed coinduced representation. This transported statement is a consequence of the cited formula, not a verbatim quotation.

View graph