Parabolic Shapiro lifting for Gamma1(N) in every coefficient degree

Proved

MTT.Cohomology.exists_parabolic_coinduced_cocycle

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

group-cohomologymodular-formsshapiro

Let $N>0$ and $n\ge0$ . Put $H=\Gamma_1(N)$ , $G=\mathrm{SL}_2(\mathbb Z)$ , and $V=\operatorname{Sym}^{n}(\mathbb C^2)$ with the MTT left action. Every parabolic one-cocycle $b:H\to V$ admits a one-cocycle $C:G\to\operatorname{Coind}_H^G V$ satisfying $C(h)(1)=b(h)$ for all $h\in H$ . The lift is parabolic: for every rational cusp $x$ and every $g\in G$ fixing $x$ , there is a coinduced vector $P$ such that $C(g)=gP-P$ . This supplies the cocycle-level parabolic compatibility needed to transport the MTT dimension problem to the full modular group. It includes degree zero and all positive levels.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.RepresentationTheory.Coinduced
set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.Cohomology.exists_parabolic_coinduced_cocycle {N n : ℕ} (hN : 0 < N)
    (b : MTT.Cohomology.parabolicCocycles N n) :
    ∃ c : groupCohomology.cocycles₁
        (Rep.coind (CongruenceSubgroup.Gamma1 N).subtype (MTT.Cohomology.gammaOneRep N n)),
      (∀ h : CongruenceSubgroup.Gamma1 N, (c h.val).val 1 = b.val h) ∧
      ∀ (x : MTT.Cohomology.Cusp) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
        MTT.Cohomology.cuspAct g x = x →
        ∃ P : Rep.coind (CongruenceSubgroup.Gamma1 N).subtype (MTT.Cohomology.gammaOneRep N n),
          c g = (Rep.coind (CongruenceSubgroup.Gamma1 N).subtype
            (MTT.Cohomology.gammaOneRep N n)).ρ g P - P := by sorry

Source

Columbia Spring 2021 Eichler-Shimura seminar notes, Section 1.1, Lemma 1 (parabolic Shapiro), page 2, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. The finite-power proof is adapted from the already-proved Gamma0 Shapiro dimension comparison 3b95e6da-4049-5a35-810c-3de89df0e00e, accepted proof c7770f6c-0e05-5212-ac9a-be8ca5205c57; the explicit degree-one transversal lift also follows accepted proof 4daf947c-3676-51e9-8e78-97c720db5c26. These platform sources originate in the FLT repository at aa2d8b34692b16c70f699536de0d8e75b9a3e9ef. The submission reproves all needed algebra under default limits, using only mathlib and the frozen MTT definition.

View graph