Eichler–Shimura injectivity: a principal mixed period cocycle has zero cusp forms

Proved

MTT.Cohomology.period_cocycle_injective

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

group-cohomologymodular-formsmodular-symbols

Let $N\ge1$ , $k\ge2$ , $n=k-2$ , and let $g,h\in S_k(\Gamma_1(N))$ . Write $P_f(x)$ for the normalized cusp primitive of $f$ : it vanishes at infinity and for $r\in\mathbf Q$ is

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

For a matrix $\gamma=\begin{pmatrix}a&b\\c&d\end{pmatrix}$ the coefficient action is $\gamma\cdot Q(X,Y)=Q(aX+cY,bX+dY)$ . Put $\rho=\operatorname{diag}(-1,1)$ ; it sends a finite cusp $r$ to $-r$ and fixes infinity.

Suppose there is a homogeneous degree- $n$ polynomial $P\in\mathbf C[X,Y]$ such that, for every $\gamma\in\Gamma_1(N)$ ,

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

Then $g=h=0$ .

Thus the sum of the holomorphic and reflected period cocycles cannot be a principal group cocycle unless both cusp forms vanish. This is the injectivity assertion in ordinary/parabolic Eichler–Shimura cohomology, expressed in the mission's homogeneous-polynomial, left-action and normalized-integral conventions. There is no hypothesis about a boundary function on all cusps or a chosen integration map.

Preamble

import Definitions.Def_MTT_Cohomology_Integration

set_option autoImplicit false
noncomputable section
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.period_cocycle_injective
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (g h : CuspForm (MTT.GammaOne N) (k : ℤ)) (P : Binary ℂ)
    (hP : P ∈ Sym ℂ (k - 2))
    (hcob : ∀ γ : CongruenceSubgroup.Gamma1 N,
      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) :
    g = 0 ∧ h = 0 := by sorry

Source

Ash–Stevens, Modular forms in characteristic ℓ and special values of their L-functions, Duke Math. J. 53 (1986), Theorem 2.3, p. 853, https://math.bu.edu/people/ghs/papers/Mod_fms_char_ell.pdf (ordinary group-cohomology Eichler–Shimura). Explicit period-cocycle construction and injectivity proof: 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. The displayed Lean formulation changes from a based interior primitive to the normalized cusp primitive, and realizes the antiholomorphic summand by reflection, as in the MTT mission.

View graph