Prove2Me

The cusp-condition codimension is at most the cusp double-coset count

Proved
MTT.Cohomology.finrank_modularForm_le_cuspForm_add_doubleCosets

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

dimensionmodular-formsmtt

Let HH be a finite-index subgroup of SL2(Z)\mathrm{SL}_2(\mathbb Z) and let k∈Zk\in\mathbb Z. Let TT be the translation matrix and put P∞=⟨T,−I⟩P_\infty=\langle T,-I\rangle. Then

dim⁡CMk(H)≤dim⁡CSk(H)+#(H\SL2(Z)/P∞).\dim_{\mathbb C} M_k(H)\le\dim_{\mathbb C} S_k(H)+\#(H\backslash\mathrm{SL}_2(\mathbb Z)/P_\infty).

This elementary codimension bound converts a modular-form dimension lower bound into a cusp-form lower bound. It is used in the higher-weight Gamma1 dimension branch of the MTT mission. No equality or cohomology comparison is asserted.

Preamble
import Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
import Mathlib.GroupTheory.DoubleCoset
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
open scoped MatrixGroups
Formal statement
theorem MTT.Cohomology.finrank_modularForm_le_cuspForm_add_doubleCosets
    (H : Subgroup SL(2, ℤ)) [H.FiniteIndex] (k : ℤ) :
    Module.finrank ℂ (ModularForm H k) ≤ Module.finrank ℂ (CuspForm H k) +
      Nat.card (DoubleCoset.Quotient (H : Set SL(2, ℤ))
        ((Subgroup.zpowers ModularGroup.T ⊔ Subgroup.zpowers (-1) : Subgroup SL(2, ℤ)) :
          Set SL(2, ℤ))) := by sorry
Source
Marc Masdeu, Modular Forms, Chapter 5, §5.1, cusp evaluations before Lemma 5.2 and Theorem 5.1 (Eisenstein codimension formulas): https://mmasdeu.github.io/modularforms/5_eisenstein.html. This is the elementary upper-bound-on-codimension part, generalized by the same evaluation argument to arbitrary finite-index subgroups and integral weights.

View graph