The eigenvalue system of a good Hecke eigenform

The eigenvalues of a good Hecke eigenform f (EigenformAwayFromLevel) inherit the multiplication table of the Γ₀(N) Hecke ring: they are multiplicative on coprime indices, and along the powers of a good prime p they satisfy the Diamond–Shurman recurrence λ_{p^{r+2}} = λ_p λ_{p^{r+1}} − χ(p) p^{k−1} λ_{p^r}, because the scalar coset T(p, p) acts on the character space by χ(p) p^{k−2}. Nothing here touches Fourier coefficients: the three identities eigenvalue_one, eigenvalue_mul and eigenvalue_prime_pow_add_two are images of relations in the ring under heckeRingHomCuspCharSpace, evaluated on the (nonzero) form; the remaining statements are consequences (a congruence in the index, the prime-square instance, and the cancellation argument below).

These identities are what the strong-multiplicity-one argument consumes: they let the eigenvalues at composite good indices be read off the eigenvalues at good primes and the character.

Main results

• HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_one: λ₁ = 1.
• HeckeRing.GL2.EigenformAwayFromLevel.heckeTCuspNat_eq_eigenvalue_smul: at a good prime the classical operator Tₚ on S_k(Γ₁(N)) acts on the form by λₚ, and HeckeRing.GL2.EigenformAwayFromLevel.heckeTCuspNat_levelRaise_eq_eigenvalue_smul: so does Tₚ at a level N with d * M ∣ N on the level-raise V_d f.
• HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_mul: λ_{mn} = λ_m λ_n for coprime good indices.
• HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_prime_pow_add_two: the recurrence along the powers of a good prime, and its first instance HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_prime_sq.
• HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_forall_prime_and_sq_eigenvalue_eq: the nebentypus is determined by the eigenvalues at the good primes and their squares, with HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_forall_eigenvalue_eq the convenience form assuming agreement at every good index. The prime case is HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_eigenvalue_eq_prime_and_sq, read off eigenvalue_prime_sq.

The statements build the coprimality proofs guarding eigenvalue from their hypotheses (Nat.coprime_mul_iff_left, Nat.Coprime.pow_left, cast along the coercion lemmas of ℕ+); by proof irrelevance they rewrite whichever proof a consumer holds, and eigenvalue_congr moves between spellings of an index.

Provenance

The multiplicativity and the prime-square identity appear as Eigenform.coeff_eq_coeff_one_mul_eigenvalue and eigenvalue_at_prime_sq_of_coeff_one_ne_zero 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), derived there from the Fourier coefficients of a normalised eigenform. Here both are read off the Hecke ring instead, so no normalisation and no coefficient formula is needed.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.8.
• T. Miyake, Modular forms, §4.6.

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_congr {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) {m n : ℕ+} (hmn : m = n) {hm : (↑m).Coprime N} {hn : (↑n).Coprime N} : f.eigenvalue m hm = f.eigenvalue n hn

The eigenvalue depends only on the index, not on the coprimality proof or on how the index is spelled.

@[simp]

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_one {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) : f.eigenvalue 1 ⋯ = 1

The eigenvalue at 1 is 1: the ring element at index 1 is the identity.

theorem HeckeRing.GL2.EigenformAwayFromLevel.heckeTCuspNat_eq_eigenvalue_smul {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : (heckeTCuspNat k p) f.toCuspForm = f.eigenvalue ⟨p, ⋯⟩ hpN • f.toCuspForm

At a good prime the classical Tₚ acts by the eigenvalue: the ring generator at p acts on the character space as heckeTCuspNat k p, so Tₚ f = λₚ f on S_k(Γ₁(N)).

theorem HeckeRing.GL2.EigenformAwayFromLevel.heckeTCuspNat_levelRaise_eq_eigenvalue_smul {N : ℕ} [NeZero N] {k : ℤ} {M d : ℕ} [NeZero M] [NeZero d] (g : EigenformAwayFromLevel M k) (h : d * M ∣ N) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : (heckeTCuspNat k p) (TauCeti.CuspForm.levelRaise d ⋯ g.toCuspForm) = g.eigenvalue ⟨p, ⋯⟩ ⋯ • TauCeti.CuspForm.levelRaise d ⋯ g.toCuspForm

V_d of a good eigenform is a good eigenvector with the same eigenvalues: for d * M ∣ N and a prime p ∤ N, Tₚ (V_d g) = λₚ(g) • V_d g at level N, since Tₚ commutes with the level-raising operator V_d (heckeTCuspNat_levelRaise).

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_mul {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) {m n : ℕ+} (hmn : (↑m).Coprime ↑n) (hm : (↑m).Coprime N) (hn : (↑n).Coprime N) : f.eigenvalue (m * n) ⋯ = f.eigenvalue m hm * f.eigenvalue n hn

Multiplicativity on coprime good indices: λ_{mn} = λ_m λ_n, the image of the coprime multiplication rule heckeTCompositeGamma0_mul_of_coprime of the Hecke ring.

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_prime_pow_add_two {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) {p : ℕ+} (hp : Nat.Prime ↑p) (hpN : (↑p).Coprime N) (r : ℕ) : f.eigenvalue (p ^ (r + 2)) ⋯ = f.eigenvalue p hpN * f.eigenvalue (p ^ (r + 1)) ⋯ - ↑(f.χ (ZMod.unitOfCoprime (↑p) hpN)) * ↑↑p ^ (k - 1) * f.eigenvalue (p ^ r) ⋯

The recurrence along the powers of a good prime: λ_{p^{r+2}} = λ_p λ_{p^{r+1}} − χ(p) p^{k−1} λ_{p^r}. This is the image of the defining recurrence of the ring on the character space (heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ_apply), evaluated on the form.

theorem HeckeRing.GL2.EigenformAwayFromLevel.eigenvalue_prime_sq {N : ℕ} [NeZero N] {k : ℤ} (f : EigenformAwayFromLevel N k) {p : ℕ+} (hp : Nat.Prime ↑p) (hpN : (↑p).Coprime N) : f.eigenvalue (p ^ 2) ⋯ = f.eigenvalue p hpN ^ 2 - ↑(f.χ (ZMod.unitOfCoprime (↑p) hpN)) * ↑↑p ^ (k - 1)

The prime-square identity: λ_{p²} = λ_p² − χ(p) p^{k−1} at a good prime.

The nebentypus is determined by the good eigenvalues

theorem HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_eigenvalue_eq_prime_and_sq {N : ℕ} [NeZero N] {k : ℤ} {f f' : EigenformAwayFromLevel N k} {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) (h₁ : f.eigenvalue ⟨p, ⋯⟩ hpN = f'.eigenvalue ⟨p, ⋯⟩ hpN) (h₂ : f.eigenvalue (⟨p, ⋯⟩ ^ 2) ⋯ = f'.eigenvalue (⟨p, ⋯⟩ ^ 2) ⋯) : f.χ (ZMod.unitOfCoprime p hpN) = f'.χ (ZMod.unitOfCoprime p hpN)

At a good prime, the character value is a function of the eigenvalues at p and p²: eigenvalue_prime_sq reads λ_{p²} = λ_p² − χ(p) p^{k−1}, so two eigenforms agreeing at those two indices have the same χ(p).

The coprimality arguments of eigenvalue are the canonical proofs built from hpN; by proof irrelevance a consumer holding some other proof of the same statement can pass it unchanged.

theorem HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_forall_prime_and_sq_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {f f' : EigenformAwayFromLevel N k} (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), f.eigenvalue ⟨p, ⋯⟩ hpN = f'.eigenvalue ⟨p, ⋯⟩ hpN ∧ f.eigenvalue (⟨p, ⋯⟩ ^ 2) ⋯ = f'.eigenvalue (⟨p, ⋯⟩ ^ 2) ⋯) : f.χ = f'.χ

The nebentypus character is determined by the eigenvalues at the good primes and their squares.

chi_eq_of_eigenvalue_eq_prime_and_sq gives the value at each good prime; it spreads to every unit because every unit of ZMod N is ZMod.unitOfCoprime m for some m coprime to N (ZMod.exists_unitOfCoprime_eq), and both sides are multiplicative in m (ZMod.unitOfCoprime_mul).

This is the eigenvalue-side counterpart of eq_of_mem_cuspFormCharSpace_of_ne_zero, which recovers the character from the underlying form.

theorem HeckeRing.GL2.EigenformAwayFromLevel.chi_eq_of_forall_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {f f' : EigenformAwayFromLevel N k} (h : ∀ (n : ℕ+) (hn : (↑n).Coprime N), f.eigenvalue n hn = f'.eigenvalue n hn) : f.χ = f'.χ

The nebentypus character is determined by the good eigenvalues, the convenience form: agreement at every index coprime to N is more than chi_eq_of_forall_prime_and_sq_eigenvalue_eq needs, and gives the same conclusion.