Large-level dimensions of central-fixed coinduction and its S, ST, T fixed spaces

Proved

MTT.Cohomology.centralCoinduced_fixed_dimensions_large_level

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

dimensionmttrepresentation-theory

Let $N\ge5$ and $n>0$ , and let $W=(\operatorname{Coind}_{\Gamma_1(N)}^{\mathrm{SL}_2(\mathbb Z)}\operatorname{Sym}^n\mathbb C^2)^{-I=1}$ . Set $\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)$ . For the standard modular generators $S,T$ , the following four assertions hold:

\dim W=(n+1)\mu,\qquad 2\dim W^S=\dim W,\qquad 3\dim W^{ST}=\dim W,\qquad c\le\dim W^T.

Here $W^g=\ker(\rho(g)-1)$ , and all dimensions are over $\mathbb C$ . These finite-coset counts supply the numerical input to the full-group parabolic-cohomology estimate. The restriction $N\ge5$ excludes elliptic stabilizers and irregular cusps; no parity condition is imposed on $n$ .

Preamble

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

Formal statement

theorem MTT.Cohomology.centralCoinduced_fixed_dimensions_large_level {N n : ℕ}
    (hN : 5 ≤ N) (hn : 0 < n) :
    let W := MTT.Cohomology.centralCoinduced N n
    Module.finrank ℂ W =
        (n + 1) * (CongruenceSubgroup.Gamma1 N ⊔ Subgroup.zpowers (-1 : SL(2, ℤ))).index ∧
      2 * Module.finrank ℂ (W.ρ ModularGroup.S - LinearMap.id).ker = Module.finrank ℂ W ∧
      3 * Module.finrank ℂ (W.ρ (ModularGroup.S * ModularGroup.T) - LinearMap.id).ker =
        Module.finrank ℂ W ∧
      Nat.card (DoubleCoset.Quotient (CongruenceSubgroup.Gamma1 N : Set SL(2, ℤ))
        ((Subgroup.zpowers ModularGroup.T ⊔ Subgroup.zpowers (-1) : Subgroup SL(2, ℤ)) :
          Set SL(2, ℤ))) ≤ Module.finrank ℂ (W.ρ ModularGroup.T - LinearMap.id).ker := by sorry

Source

Finite-orbit coefficient count underlying the cohomological calculation 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, with the absence of elliptic points and irregular cusps for N>=5 recorded by Stein, Modular Forms: A Computational Approach, Chapter 6 Proposition 6.6, https://wstein.org/books/modform/modform/dimension_formulas.html. This is a transported finite-coset consequence, not a verbatim source statement. Related proved Gamma0 finite-orbit calculation: HeckeEis.le_finrank_fixed_induced_binaryFormRepSL, 97044c7f-6184-5086-9b7d-a2178cc068c0; its Gamma0/even hypotheses cannot be substituted directly for the present Gamma1 central-fixed representation.

View graph