6. Strong multiplicity one
(New-part identity — Miyake 4.6.12, new part.) If f is a normalised newform and
g^{(1)} is a common eigenfunction in the new subspace of S_k(N, \chi) sharing f's
eigenvalues off a finite set, then g^{(1)} = a_1(g^{(1)})\, f
(Definition 5.2, Theorem 3.2, Theorem 3.3).
Lean code for Theorem6.1●1 theorem
Associated Lean declarations
If g^{(1)} = 0 this is trivial; otherwise b_1 = a_1(g^{(1)}) \ne 0 by
Theorem 3.3. Sharing eigenvalues off a finite set forces all coprime
eigenvalues to agree (propagated by multiplicativity, Theorem 2.3).
Then h = b_1^{-1} g^{(1)} - f has a_n(h) = \lambda_n - \lambda_n = 0 for all
\gcd(n, N) = 1 (Theorem 3.2 with a_1(f) = 1), so h is old by
Theorem 5.1; being a difference of new forms it is also new, hence h = 0.
(Old-part vanishing — Miyake 4.6.12, steps (i)–(ii).) If f is a nonzero newform and
g^{(2)} is a common eigenfunction in the (\chi-refined) old subspace sharing f's
eigenvalues off a finite set, then g^{(2)} = 0
(Definition 5.2, Theorem 4.8, Theorem 5.3).
Lean code for Theorem6.2●1 theorem
Associated Lean declarations
Suppose g^{(2)} \ne 0. Write it in the descent normal form
(Theorem 4.8) as a sum of level-raised new eigenforms; the
summands whose eigenvalues differ from f's are Petersson-orthogonal
(Definition 4.4) and drop out, leaving a nonzero new eigenform h at a proper
divisor sharing f's eigenvalues. Its leading coefficient is nonzero
(Theorem 3.3), so h minus a scalar multiple of f has vanishing
coprime coefficients hence is old (Theorem 5.1); but h is old and f is not
(Theorem 5.3), a contradiction.
(Strong multiplicity one, constant-multiple form — Miyake Theorem 4.6.12.) Let f be a
normalised newform in S_k(N, \chi) and g any cusp-form Hecke eigenfunction in
S_k(N, \chi). If f and g share the eigenvalue \lambda_n for all but finitely
many \gcd(n, N) = 1, then g = c\, f for a single c \in \mathbb{C}
(Definition 5.2, Theorem 6.1, Theorem 6.2).
Lean code for Theorem6.3●1 theorem
Associated Lean declarations
-
theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.leancomplete
theorem HeckeRing.GL2.strongMultiplicityOne_constMul {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (g : HeckeRing.GL2.Eigenform N k) (χ : (ZMod N)ˣ →* ℂˣ) (hfχ : f.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (S : Finset ℕ) (h_eig : ∀ (n : ℕ+), (↑n).Coprime N → ↑n ∉ S → f.eigenvalue n = g.eigenvalue n) : ∃ c, g.toCuspForm = c • f.toCuspForm
theorem HeckeRing.GL2.strongMultiplicityOne_constMul {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (g : HeckeRing.GL2.Eigenform N k) (χ : (ZMod N)ˣ →* ℂˣ) (hfχ : f.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (S : Finset ℕ) (h_eig : ∀ (n : ℕ+), (↑n).Coprime N → ↑n ∉ S → f.eigenvalue n = g.eigenvalue n) : ∃ c, g.toCuspForm = c • f.toCuspForm
**Miyake Theorem 4.6.12 (Strong Multiplicity One, full constant-multiple form).** If `f` is a normalised `Newform` at level `N` with Nebentypus `χ` and `g` is a common `T(n)`-eigenfunction in `S_k(Γ₁(N), χ)` sharing `f`'s eigenvalues off a finite set `S`, then `g = c • f` for some `c ∈ ℂ`.
Split g = g^{(1)} + g^{(2)} along the orthogonal new/old decomposition
(Definition 4.5). Both parts are again common eigenfunctions sharing f's
eigenvalues (Theorem 4.7). The new part is a_1(g^{(1)})\, f by
Theorem 6.1, and the old part vanishes by Theorem 6.2
(after identifying the two old spaces on the \chi-isotypic part,
Theorem 4.9). Hence g = a_1(g)\, f.
(Strong multiplicity one — Miyake Theorem 4.6.8 / 4.6.12.) Two newforms f, g in the
same Nebentypus space S_k(N, \chi) whose Hecke eigenvalues \lambda_n agree for all
but finitely many n are equal (Definition 5.2, Theorem 6.3). In
LeanModularForms this is the axiom-clean headline
\texttt{strongMultiplicityOne\_axiom\_clean}.
Lean code for Theorem6.4●1 theorem
Associated Lean declarations
-
theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.leancomplete
theorem HeckeRing.GL2.strongMultiplicityOne_axiom_clean {N : ℕ} [NeZero N] {k : ℤ} (f g : HeckeRing.GL2.Newform N k) (χ : (ZMod N)ˣ →* ℂˣ) (hfχ : f.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (S : Finset ℕ) (h_eig : ∀ (n : ℕ+), (↑n).Coprime N → ↑n ∉ S → f.eigenvalue n = g.eigenvalue n) : f.toCuspForm = g.toCuspForm
theorem HeckeRing.GL2.strongMultiplicityOne_axiom_clean {N : ℕ} [NeZero N] {k : ℤ} (f g : HeckeRing.GL2.Newform N k) (χ : (ZMod N)ˣ →* ℂˣ) (hfχ : f.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (S : Finset ℕ) (h_eig : ∀ (n : ℕ+), (↑n).Coprime N → ↑n ∉ S → f.eigenvalue n = g.eigenvalue n) : f.toCuspForm = g.toCuspForm
**Strong Multiplicity One for both newforms (DS 5.8.2.1).** Two `Newform`s at level `N` in the same Nebentypus eigenspace with equal eigenvalues outside a finite set `S` are equal. Corollary of `strongMultiplicityOne_constMul` (T014): the constant multiple it returns is forced to be `1` since both newforms are normalised (`a₁ = 1`).
By Theorem 6.3 there is c with g = c\, f. Comparing first Fourier
coefficients and using that both newforms are normalised, 1 = a_1(g) = c\, a_1(f) = c,
so c = 1 and f = g.