Strong multiplicity one

Two newforms of level N, weight k and the same nebentypus whose eigenvalues agree at every prime p ∤ 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 primes dividing the level, nor at finitely many good primes, and so in particular at finitely many good indices.

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 difference of the two underlying cusp forms is a Hecke eigenvector, with a₁ = 0, at every prime not dividing P N, where P is the product of the exceptional primes; its coefficients therefore vanish at every index coprime to P N. A prime away from the level can be dropped from that condition (TauCeti.qExpansion_coeff_eq_zero_of_forall_coprime_mul), so they vanish at every index coprime to N, and the difference 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, at the good indices outside a finite set. Those coefficients also determine the nebentypus, so that form needs no hypothesis on it (Newform.eq_of_forall_notMem_qExpansion_coeff_eq, in TauCeti.NumberTheory.ModularForms.Newforms.StrongMultiplicityOne.Nebentypus, together with its cross-level analogue).

Across unrelated levels, two newforms f, g of levels N, M whose nebentypes induce the same character modulo lcm N M and whose eigenvalues agree at all but finitely many primes p ∤ N M have N = M (Newform.level_eq_of_forall_notMem_prime_eigenvalue_eq). Nothing is assumed at the primes dividing N M; the two forms are separated by the q-new subspaces (TauCeti.cuspFormsNewAt) at a prime q where the levels have different valuations. At equal levels the fixed-level theorem then makes them the same function (Newform.level_eq_and_coe_eq_of_forall_notMem_prime_eigenvalue_eq).

Main results

• HeckeRing.GL2.Newform.eq_of_forall_notMem_prime_eigenvalue_eq: strong multiplicity one, on the eigenvalues at the primes outside a finite set.
• 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.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.
• HeckeRing.GL2.Newform.level_eq_of_forall_notMem_prime_eigenvalue_eq: two newforms of levels N and M with compatible nebentypes whose eigenvalues agree at all but finitely many primes p ∤ N M have N = M (Miyake, Theorem 4.6.19, for newforms).
• HeckeRing.GL2.Newform.level_eq_and_coe_eq_of_forall_notMem_prime_eigenvalue_eq: under the same hypotheses, N = M and the two newforms are the same function.
• HeckeRing.GL2.Newform.level_eq_and_coe_eq_of_comp_unitsMap_eq: two newforms of levels dividing N, with nebentypes inducing the same character modulo N and eigenvalues agreeing at all but finitely many primes p ∤ N, have the same level and are the same function (Miyake, Corollary 4.6.20; Diamond–Shurman, Theorem 5.8.3).

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. The source excepts finitely many good indices; excepting finitely many primes instead, by dropping them from the coprimality condition on the coefficients, is not taken from there. Neither is the comparison across unrelated levels, which follows the q-new decomposition of Atkin–Lehner and Li.

References

• T. Miyake, Modular forms, Theorem 4.6.12, Theorem 4.6.19 for the cross-level statement, and Corollary 4.6.20 for the uniqueness of the associated newform.
• W.-C. W. Li, Newforms and functional equations, Math. Ann. 212 (1975), 285–315, for the comparison across levels through the q-new subspaces.
• 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), and Theorem 5.8.3 for the uniqueness of the associated newform.

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

Strong multiplicity one at the primes (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 prime p ∤ N outside a finite set S are equal. Nothing is assumed at the primes dividing N, nor at the primes of S.

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.

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.

Across unrelated levels

theorem HeckeRing.GL2.Newform.level_eq_of_forall_notMem_prime_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {M : ℕ} [NeZero M] (f : Newform N k) (g : Newform M k) (hχ : f.χ.comp (ZMod.unitsMap ⋯) = g.χ.comp (ZMod.unitsMap ⋯)) {S : Finset ℕ} (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N) (hpM : p.Coprime M), p ∉ S → f.eigenvalue ⟨p, ⋯⟩ hpN = g.eigenvalue ⟨p, ⋯⟩ hpM) : N = M

Strong multiplicity one across levels, the level (Miyake, Theorem 4.6.19, for newforms). Let f, g be newforms of the same weight and of levels N, M whose nebentypes induce the same character modulo lcm N M, and whose eigenvalues agree at every prime p ∤ N M outside a finite set S. Then N = M.

Nothing is assumed at the primes dividing N M, nor at the finitely many primes of S. With N = M in hand, Newform.eq_of_forall_prime_eigenvalue_eq gives f = g when the eigenvalues agree at every good prime.

theorem HeckeRing.GL2.Newform.level_eq_and_coe_eq_of_forall_notMem_prime_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ} {M : ℕ} [NeZero M] (f : Newform N k) (g : Newform M k) (hχ : f.χ.comp (ZMod.unitsMap ⋯) = g.χ.comp (ZMod.unitsMap ⋯)) {S : Finset ℕ} (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N) (hpM : p.Coprime M), p ∉ S → f.eigenvalue ⟨p, ⋯⟩ hpN = g.eigenvalue ⟨p, ⋯⟩ hpM) : N = M ∧ ⇑f.toCuspForm = ⇑g.toCuspForm

Strong multiplicity one across levels (Miyake, Theorem 4.6.19, for newforms). Let f, g be newforms of the same weight and of levels N, M whose nebentypes induce the same character modulo lcm N M, and whose eigenvalues agree at every prime p ∤ N M outside a finite set S. Then N = M and f and g are the same function on ℍ.

Nothing is assumed at the primes dividing N M, nor at the finitely many primes of S. The level is Newform.level_eq_of_forall_notMem_prime_eigenvalue_eq; at equal levels the compatibility of the nebentypes is their equality, and Newform.eq_of_forall_notMem_prime_eigenvalue_eq applies.

theorem HeckeRing.GL2.Newform.level_eq_and_coe_eq_of_comp_unitsMap_eq {N : ℕ} [NeZero N] {k : ℤ} {M M' : ℕ} [NeZero M] [NeZero M'] {χ : (ZMod N)ˣ →* ℂˣ} (g : Newform M k) (g' : Newform M' k) (hM : M ∣ N) (hM' : M' ∣ N) (hgχ : g.χ.comp (ZMod.unitsMap hM) = χ) (hg'χ : g'.χ.comp (ZMod.unitsMap hM') = χ) {S : Finset ℕ} (h : ∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), p ∉ S → g.eigenvalue ⟨p, ⋯⟩ ⋯ = g'.eigenvalue ⟨p, ⋯⟩ ⋯) : M = M' ∧ ⇑g.toCuspForm = ⇑g'.toCuspForm

Uniqueness of the newform with a given good eigensystem and nebentypus. Let g and g' be newforms of levels M and M' dividing N, whose nebentypes induce the same character χ modulo N. If their eigenvalues agree at every prime p ∤ N outside a finite set S, then M = M' and g and g' are the same function. This is the uniqueness of the newform associated with a good Hecke eigenform (Diamond–Shurman, Theorem 5.8.3; Miyake, Corollary 4.6.20).