Injective Hecke-equivariant integration map

Proved

MTT.Cohomology.integration_map

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

group-cohomologymodular-formsperiods

There is an injective complex-linear integration map from weight-k cusp forms to compactly supported group cohomology, with its cuspidal image as target subspace. It intertwines the explicitly normalized prime-Hecke formulas. Evaluation of the X^jY^(k−2−j) coefficient at [∞]−[r] equals binomial(k−2,j) times the existing MTT modular integral. The integration normalization is −2πi. Injectivity is explicitly an open obligation.

Preamble

import Definitions.Def_MTT_Cohomology
import Mathlib.RingTheory.Flat.Basic
set_option autoImplicit false
noncomputable section
open scoped BigOperators TensorProduct
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.integration_map
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k) :
    ∃ I : CuspForm (MTT.GammaOne N) (k : ℤ) →ₗ[ℂ] Hc N (k-2) ℂ,
      Function.Injective I ∧ HeckeEquivariant I ∧ ∀ f, IntegralClass f (I f) := by sorry

Source

Shimura, Introduction to the Arithmetic Theory of Automorphic Functions (1971), Chapter 8; Ash–Stevens Theorem 2.3, p. 853. Full prime Hecke operators (including bad primes) and nebentype are retained; multiplicity one and exclusion of boundary eigensystems are part of this target. For the integral formula, Ash–Stevens §4, pp. 863–864.

View graph