Prove2Me

Finite right-coset representatives for Γ1(N)\Gamma_1(N)

Proved
MTT.Cohomology.gammaOne_has_finset_complement

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

group-theorymodular-formsperiods

Let N>0N>0. There is a finite set R⊆SL2(Z)R\subseteq \mathrm{SL}_2(\mathbb Z) containing exactly one representative of every right coset of Γ1(N)\Gamma_1(N): multiplication induces a bijection

Γ1(N)×R  ⟶  SL2(Z).\Gamma_1(N)\times R\;\longrightarrow\;\mathrm{SL}_2(\mathbb Z).

This is the finite-coset interface used to express integrals over Γ1(N)\H\Gamma_1(N)\backslash\mathfrak H as finite sums over translates of the standard modular fundamental domain.

Formalization Note The uniqueness and coverage conditions are packaged by Mathlib's Subgroup.IsComplement.

Preamble
import Definitions.Def_MTT_PeriodPairing

set_option autoImplicit false
noncomputable section
open scoped MatrixGroups
Formal statement
theorem MTT.Cohomology.gammaOne_has_finset_complement
    {N : ℕ} (hN : 0 < N) :
    ∃ R : Finset (Matrix.SpecialLinearGroup (Fin 2) ℤ),
      Subgroup.IsComplement
        (CongruenceSubgroup.Gamma1 N : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ))
        (R : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)) := by sorry
Source
Classical finite-index property of congruence subgroups; Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, proof of Theorem 1, pp. 7–10, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf.

View graph