Multiplicity at most one for each signed cuspidal eigenpacket

Proved

MTT.Cohomology.signed_packet_multiplicity_one

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

group-cohomologymodular-formsperiods

Any two compactly supported cohomology classes with the same sign, nebentype and full prime eigenpacket of the given cuspidal eigenform are linearly dependent. This is a separate Eichler–Shimura/multiplicity-one obligation: it is not inferred from injectivity alone. It includes arbitrary eigenforms at the stated level, not only newforms.

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.signed_packet_multiplicity_one
    {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
    (s : Bool) (φ ψ : Hc N (k-2) ℂ)
    (hφ : Packet (fun d => ι (f.epsilon d)) (fun l => ι (f.coeff l)) s φ)
    (hψ : Packet (fun d => ι (f.epsilon d)) (fun l => ι (f.coeff l)) s ψ) :
    ∃ a b : ℂ, (a ≠ 0 ∨ b ≠ 0) ∧ a • φ + b • ψ = 0 := 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.

View graph