Strong multiplicity one, at fixed level and nebentypus

Two newforms of level N, weight k and the same nebentypus whose eigenvalues agree at every index coprime to N outside a finite set are equal (Miyake, Theorem 4.6.12). The finite slack is what makes the statement strong: nothing at all is assumed at the indices dividing the level.

The same argument, run on f - a₁(g)⁻¹ V₁ g (the level-raise of g renormalised to a₁ = 1) instead of f - g, rigidifies the level across divisors: a good Hecke eigenform g of a level M ∣ N with a₁(g) ≠ 0 whose nebentypus induces that of a newform f of level N, and whose eigenvalues agree with those of f at every prime p ∤ N, has M = N (Newform.level_eq_of_dvd_of_forall_prime_eigenvalue_eq). This is the divisor-level case of strong multiplicity one across levels (Miyake, Theorem 4.6.19), with agreement asked at every good prime rather than outside a finite set.

The agreement extends from the complement of the finite set to every good index (EigenformAwayFromLevel.eigenvalue_eq_of_forall_notMem), so the difference of the two underlying cusp forms is a good Hecke eigenvector with a₁ = 0; its coefficients therefore vanish at every index coprime to N, so it is old by the Main Lemma (TauCeti.mem_cuspFormsOld_of_forall_coprime_qExpansion_coeff_eq_zero). Being a difference of newforms it is also new, and old and new are disjoint, so it is zero.

Miyake states the theorem on the Fourier coefficients rather than the eigenvalues; for a normalised newform the coefficient at a good index is the eigenvalue there (EigenformAwayFromLevel.qExpansion_coeff_eq_eigenvalue with Newform.isNorm), so that form is a corollary.

Main results

• HeckeRing.GL2.Newform.eq_of_forall_prime_eigenvalue_eq: a newform is determined by its eigenvalues at the primes not dividing the level.
• HeckeRing.GL2.Newform.eq_of_forall_notMem_eigenvalue_eq: strong multiplicity one, on the eigenvalues.
• HeckeRing.GL2.Newform.eq_of_forall_notMem_qExpansion_coeff_eq: Miyake's own form, on the q-expansion coefficients.
• HeckeRing.GL2.Newform.level_eq_of_dvd_of_forall_prime_eigenvalue_eq: a good Hecke eigenform of a divisor level M ∣ N with a₁ ≠ 0 sharing the nebentypus and the good eigensystem of a newform of level N has M = N.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bd), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/ConstantMultiple.lean — declaration strongMultiplicityOne. The source routes through strongMultiplicityOne_constMul (a newform and an eigenform sharing eigenvalues are proportional, with a₁ = 1 pinning the constant); here the difference is shown to be zero directly from the Main Lemma and the disjointness of the old and new subspaces, so the proportionality step is not needed.

References

• T. Miyake, Modular forms, Theorem 4.6.12, and Theorem 4.6.19 for the cross-level statement.
• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2 (the ∀ n coprime version; the strong form is deferred to Miyake).

theorem HeckeRing.GL2.Newform.eq_of_forall_prime_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} (hχ : f.χ = g.χ) (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), f.eigenvalue ⟨p, ⋯⟩ hpN = g.eigenvalue ⟨p, ⋯⟩ hpN) : f = g

A newform is determined by its eigenvalues at the good primes: two newforms of level N, weight k and the same nebentypus with the same eigenvalue at every prime not dividing N are equal.

theorem HeckeRing.GL2.Newform.eq_of_forall_notMem_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} (hχ : f.χ = g.χ) {S : Finset ℕ} (h : ∀ (n : ℕ+) (hn : (↑n).Coprime N), ↑n ∉ S → f.eigenvalue n hn = g.eigenvalue n hn) : f = g

Strong multiplicity one (Miyake, Theorem 4.6.12, fixed level and nebentypus): two newforms of level N, weight k and the same nebentypus whose eigenvalues agree at every index coprime to N outside a finite set are equal.

theorem HeckeRing.GL2.Newform.eq_of_forall_notMem_qExpansion_coeff_eq {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} (hχ : f.χ = g.χ) {S : Finset ℕ} (h : ∀ (n : ℕ+), (↑n).Coprime N → ↑n ∉ S → (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑g.toCuspForm)) : f = g

Strong multiplicity one, on Fourier coefficients (Miyake's own form of Theorem 4.6.12): two newforms of level N, weight k and the same nebentypus whose q-expansion coefficients agree at every index coprime to N outside a finite set are equal. For a normalised newform the coefficient at a good index is the eigenvalue there (HeckeRing.GL2.EigenformAwayFromLevel.qExpansion_coeff_eq_eigenvalue), so this is the eigenvalue form.

Across divisor levels

theorem HeckeRing.GL2.Newform.level_eq_of_dvd_of_forall_prime_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {M : ℕ} [NeZero M] (f : Newform N k) (g : EigenformAwayFromLevel M k) (hg₁ : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑g.toCuspForm) ≠ 0) (hMN : M ∣ N) (hχ : g.χ.comp (ZMod.unitsMap hMN) = f.χ) (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), g.eigenvalue ⟨p, ⋯⟩ ⋯ = f.eigenvalue ⟨p, ⋯⟩ hpN) : M = N

A good Hecke eigenform of a divisor level with a₁ ≠ 0 that shares the nebentypus and the good eigensystem of a newform of level N has level N. If g is a good Hecke eigenform of level M ∣ N with a₁(g) ≠ 0 whose nebentypus induces that of the newform f of level N, and whose eigenvalue agrees with that of f at every prime not dividing N, then M = N. Nothing requires g to be new; for a newform g the hypothesis on a₁ is Newform.isNorm.

Compare Miyake, Theorem 4.6.19 (strong multiplicity one across levels, for newforms): this is its divisor-level case, with agreement asked at every good prime rather than outside a finite set.