Parabolic Eichler–Shimura surjectivity in explicit period-cocycle form

Proved

MTT.Cohomology.parabolic_period_cocycle_surjective

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

group-cohomologymodular-formsmodular-symbols

Let $N\ge1$ , $k\ge2$ , $n=k-2$ , $\Gamma=\Gamma_1(N)$ , and $V_n$ be the homogeneous degree- $n$ polynomials in $\mathbf C[X,Y]$ . Use the left action

\begin{pmatrix}a&b\\c&d\end{pmatrix}\cdot Q(X,Y)=Q(aX+cY,bX+dY).

Let $c:\Gamma\to V_n$ be a group cocycle, so

c(\gamma\delta)=c(\gamma)+\gamma\cdot c(\delta).

Assume it is parabolic: whenever $\gamma$ fixes a cusp $x\in\mathbf P^1(\mathbf Q)$ , there is $Q\in V_n$ with $c(\gamma)=\gamma\cdot Q-Q$ .

For a cusp form $f$ , let $P_f(\infty)=0$ and

P_f(r)=2\pi\int_0^\infty f(r+it)((r+it)X+Y)^n\,dt\quad(r\in\mathbf Q).

Write $\rho=\operatorname{diag}(-1,1)$ , acting by $r\mapsto-r$ on finite cusps and fixing infinity. Then there exist $g,h\in S_k(\Gamma)$ and $P\in V_n$ such that, for all $\gamma\in\Gamma$ ,

c(\gamma)=P_g(\gamma\infty)+\rho\cdot P_h(\rho\gamma\infty)+\gamma\cdot P-P.

Thus every parabolic group-cohomology class is represented by holomorphic and reflected cusp-form periods. The principal correction $P$ makes the statement an equality of cocycles, not merely of cohomology classes.

Preamble

import Definitions.Def_MTT_Cohomology_Integration

set_option autoImplicit false
noncomputable section
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.parabolic_period_cocycle_surjective
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (c : CongruenceSubgroup.Gamma1 N → Binary ℂ)
    (hsym : ∀ γ, c γ ∈ Sym ℂ (k - 2))
    (hcoc : ∀ γ δ, c (γ * δ) = c γ + act γ.val.val (c δ))
    (hpar : ∀ (x : Cusp) (γ : CongruenceSubgroup.Gamma1 N), cuspAct γ.val x = x →
      ∃ Q : Binary ℂ, Q ∈ Sym ℂ (k - 2) ∧ c γ = act γ.val.val Q - Q) :
    ∃ (g h : CuspForm (MTT.GammaOne N) (k : ℤ)) (P : Binary ℂ),
      P ∈ Sym ℂ (k - 2) ∧ ∀ γ : CongruenceSubgroup.Gamma1 N,
        c γ = cuspPrimitive g (cuspAct γ.val OnePoint.infty) +
          act !![-1, 0; 0, 1] (cuspPrimitive h
            (fractional !![-1, 0; 0, 1] (cuspAct γ.val OnePoint.infty))) +
          (act γ.val.val P - P) := by sorry

Source

Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, Theorem 1, pp. 8–10, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf (parabolic Eichler–Shimura isomorphism; §1.1 defines parabolic cocycles). Ash–Stevens, Modular forms in characteristic ℓ and special values of their L-functions, Duke Math. J. 53 (1986), Theorem 2.3, p. 853 and Proposition 4.2, p. 862, https://math.bu.edu/people/ghs/papers/Mod_fms_char_ell.pdf. This specializes the parabolic isomorphism to Gamma1(N), reexpresses the standard symmetric power as homogeneous binary polynomials, uses the normalized cusp primitive as basepoint convention, and parametrizes the antiholomorphic summand by reflection.

View graph