Eichler–Shimura decomposition with Hecke operators at every prime

For every nonzero level and weight at least two, the holomorphic and antiholomorphic Eichler–Shimura maps are injective and have complementary images in parabolic cohomology. The cohomological Hecke operators are supplied, together with their action on arbitrary parabolic cocycle representatives. Both maps intertwine these operators with T_ℓ away from the level and U_ℓ at primes dividing the level.

This combines the FLT decomposition theorem with general Hecke descent and the intertwining identity for binary-form coefficients; no descent hypothesis is required from the caller.

theorem HeckeEis.exists_eichlerShimura_heckeEquivariant (N : ℕ) [NeZero N] (n : ℕ) : ∃ (ES : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2) →ₗ[ℂ] coeffH1par (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype)) (ESbar : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2) →ₗ⋆[ℂ] coeffH1par (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype)) (T : (ℓ : ℕ) → Nat.Prime ℓ → coeffH1par (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype) →ₗ[ℂ] coeffH1par (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype)), Function.Injective ⇑ES ∧ Function.Injective ⇑ESbar ∧ IsCompl ES.range ESbar.range ∧ (∀ (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (z : ↥(coeffParabolicCocycles (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype))), ∃ (w : ↥(coeffParabolicCocycles (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype))), ↑w = coeffHeckeFun N ℓ (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype) (binaryFormAlphaAdj ℂ n ℓ) ↑z ∧ (T ℓ hℓ) ((coeffH1parMk (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype)) z) = (coeffH1parMk (MonoidHom.comp (binaryFormRepSL ℂ n) (CongruenceSubgroup.Gamma0 N).subtype)) w) ∧ (∀ (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓN : ¬ℓ ∣ N), (∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2)), (T ℓ hℓ) (ES f) = ES ((CuspForm.heckeTLin (↑n + 2) hℓ hℓN) f)) ∧ ∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2)), (T ℓ hℓ) (ESbar f) = ESbar ((CuspForm.heckeTLin (↑n + 2) hℓ hℓN) f)) ∧ ∀ (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓN : ℓ ∣ N), (∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2)), (T ℓ hℓ) (ES f) = ES ((CuspForm.heckeULin (↑n + 2) hℓN) f)) ∧ ∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) (↑n + 2)), (T ℓ hℓ) (ESbar f) = ESbar ((CuspForm.heckeULin (↑n + 2) hℓN) f)

The Eichler–Shimura decomposition, with descended Hecke operators and compatibility at every prime, including primes dividing the level.