Eigenvalues agreeing outside a finite set agree at every good index

Strong multiplicity one, in the form proved in AINTLIB, assumes that two eigenforms have the same eigenvalue at every index coprime to the level outside a finite exceptional set; Miyake's own hypothesis (Theorem 4.6.12) is agreement at every index prime to an auxiliary level L. This file is the step that reduces the finite-exceptional-set hypothesis to agreement at every index coprime to the level: for such an index n, pick a prime q beyond the exceptional set, the level and n; the two forms agree at n q and at q, or at n q² and at q², and multiplicativity cancels the factor at q or q² — one of λ_q, λ_{q²} is nonzero, since λ_q = 0 forces λ_{q²} = −χ(q) q^{k−1} ≠ 0. Nothing compares the weights of the two forms, so they may differ, and nothing uses primality of n.

Main results

• HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_eq_of_forall_notMem: two good Hecke eigenforms of level N (of any two weights) whose eigenvalues agree at every index coprime to N outside a finite set agree at every index coprime to N.

Provenance

The argument is the opening step of strongMultiplicityOne in the AINTLIB LeanModularForms project (LeanModularForms/StrongMultiplicityOne/ConstantMultiple.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), stated there on Fourier coefficients of normalised eigenforms; here it is read off the eigenvalue system of Newforms/RingEigenvalue.lean, so no normalisation is needed.

References

• T. Miyake, Modular forms, Theorem 4.6.12.

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_eq_of_forall_notMem {N : ℕ} [NeZero N] {k₁ k₂ : ℤ} {f : EigenformAwayFromLevel N k₁} {g : EigenformAwayFromLevel N k₂} {S : Finset ℕ} (h : ∀ (n : ℕ+) (hn : (↑n).Coprime N), ↑n ∉ S → f.eigenvalue n hn = g.eigenvalue n hn) {p : ℕ+} (hpN : (↑p).Coprime N) : f.eigenvalue p hpN = g.eigenvalue p hpN

Agreement outside a finite set forces agreement at every good index. If two good Hecke eigenforms of level N, of any weights, have the same eigenvalue at every index coprime to N outside a finite set S, they have the same eigenvalue at every index p coprime to N. This is the first step of strong multiplicity one: the finite exceptional set is removed before the descent argument runs.