Large-level parabolic cohomology: the index-minus-cusps dimension bound

Proved

MTT.Cohomology.parabolicH1_dimension_upper_bound_large_level

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

dimensiongroup-cohomologymtt

Let $N\ge5$ and $k\ge3$ . Put $\mu=[\mathrm{SL}_2(\mathbb Z):\langle\Gamma_1(N),-I\rangle]$ and $c=\#(\Gamma_1(N)\backslash\mathrm{SL}_2(\mathbb Z)/\langle T,-I\rangle)$ . Then

6\dim_{\mathbb C}H^1_{\mathrm{par}}(\Gamma_1(N),\mathrm{Sym}^{k-2}\mathbb C^2)+6c\le(k-1)\mu.

This is the purely cohomological upper-bound half of the torsion-free, regular-cusp dimension comparison. The intended route uses parabolic Shapiro and the fixed spaces of S, ST and T in the central-positive coinduced representation. This theorem is explicitly OPEN; the independent cusp-form lower bound does not prove it.

Preamble

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

Formal statement

theorem MTT.Cohomology.parabolicH1_dimension_upper_bound_large_level {N k : ℕ}
    (hN : 5 ≤ N) (hk : 3 ≤ k) :
    6 * Module.finrank ℂ (MTT.Cohomology.ParabolicH1 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.

View graph