Cusp lower bound for the central coinduced T-fixed space

Proved

MTT.Cohomology.centralCoinduced_T_fixed_cusp_lower_bound

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

number-theoryrepresentation-theory

For $N\ge5$ and $n>0$ , let $W$ be the central-fixed coinduced degree- $n$ binary-form representation attached to $\Gamma_1(N)$ . The number of cusp double cosets $\Gamma_1(N)\backslash\mathrm{SL}_2(\mathbb Z)/\langle T,-I\rangle$ is at most $\dim_{\mathbb C}\ker(\rho_W(T)-1)$ . This is the remaining parabolic fixed-space input after the coefficient and elliptic fixed dimensions are computed.

Preamble

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

Formal statement

theorem MTT.Cohomology.centralCoinduced_T_fixed_cusp_lower_bound {N n : ℕ}
    (hN : 5 ≤ N) (hn : 0 < n) :
    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 ℂ ((MTT.Cohomology.centralCoinduced N n).ρ ModularGroup.T -
        LinearMap.id).ker := by sorry

Source

Residual cusp fixed-space input in MTT frontier bb6b5766-fb31-4de5-9462-40a64feda1a8; the central action must be retained also for odd symmetric powers.

View graph