Central coinduced coefficient and elliptic fixed-space dimensions

Proved

MTT.Cohomology.centralCoinduced_elliptic_dimensions

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

number-theoryrepresentation-theory

Let $N\ge5$ and $n\ge0$ , and let $W$ be the subrepresentation fixed by the central element $-I$ in the coinduction of the degree- $n$ binary-form representation from $\Gamma_1(N)$ to $\mathrm{SL}_2(\mathbb Z)$ . Write $\mu=[\mathrm{SL}_2(\mathbb Z):\langle\Gamma_1(N),-I\rangle]$ . Then $\dim W=(n+1)\mu$ , $2\dim\ker(S-1)=\dim W$ , and $3\dim\ker(ST-1)=\dim W$ . These are the first three identities in the MTT large-level fixed-dimension calculation.

Preamble

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

Formal statement

theorem MTT.Cohomology.centralCoinduced_elliptic_dimensions {N n : ℕ} (hN : 5 ≤ N) :
    Module.finrank ℂ (centralCoinduced N n) =
        (n + 1) * (CongruenceSubgroup.Gamma1 N ⊔ Subgroup.zpowers (-1 : SL(2, ℤ))).index ∧
      2 * Module.finrank ℂ ((centralCoinduced N n).ρ ModularGroup.S - LinearMap.id).ker =
        Module.finrank ℂ (centralCoinduced N n) ∧
      3 * Module.finrank ℂ
        ((centralCoinduced N n).ρ (ModularGroup.S * ModularGroup.T) - LinearMap.id).ker =
        Module.finrank ℂ (centralCoinduced N n) := by sorry

Source

Finite-dimensional cyclic averaging and trace calculation, with the Gamma1 trace congruence modulo N; supporting lemma for MTT frontier bb6b5766-fb31-4de5-9462-40a64feda1a8.

View graph