Existence of the Hecke-equivariant integration map
ProvedMTT.Cohomology.integration_map_existsgroup-cohomologymodular-formsmodular-symbolsnumber-theory
There is a complex-linear map from weight-k cusp forms of level N to compactly supported group cohomology with degree k-2 binary polynomial coefficients, intertwining the explicitly normalized prime Hecke operators, whose coefficient evaluation on the path from infinity to a rational cusp r equals binomial(k-2,j) times the modular integral of f against X^j at r. Injectivity is deliberately not asserted: this node isolates the analytic construction of the class, namely that the path integral of f(z)(zX+Y)^(k-2) is a Gamma-equivariant cocycle on pairs of cusps.
Preamble
import Definitions.Def_MTT_Cohomology set_option autoImplicit false noncomputable section open scoped BigOperators open MTT.Cohomology
Formal statement
theorem MTT.Cohomology.integration_map_exists
{N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k) :
∃ I : CuspForm (MTT.GammaOne N) (k : ℤ) →ₗ[ℂ] Hc N (k - 2) ℂ,
HeckeEquivariant I ∧ ∀ f, IntegralClass f (I f) := by sorrySource
Shimura, Introduction to the arithmetic theory of automorphic functions, Ch. 8; Mazur-Tate-Teitelbaum, Invent. Math. 84 (1986), Theorem 2.3 and §4