Multiplicity one on the new part of S_k(N, χ)

A cusp form in the new part of S_k(N, χ) that is an eigenvector of the Hecke ring at every prime not dividing N is determined, up to a scalar, by those eigenvalues. Equivalently: each simultaneous eigenspace of the good Hecke operators inside S_k(N, χ)ⁿᵉʷ is at most one-dimensional, and is a line as soon as it is nonzero.

It rests on eq_zero_of_forall_prime_heckeRingHomCusp_of_one_eq_zero_of_mem_cuspFormsNew (Newforms/EigenvectorVanishing.lean): such an eigenvector with a₁ = 0 is zero. Scaling each of the two eigenvectors by the other's first coefficient and subtracting produces exactly such an eigenvector.

Main results

• HeckeRing.GL2.smul_eq_smul_of_forall_prime_heckeRingHomCusp_of_mem_cuspFormsNew: two good Hecke eigenvectors in the new part sharing their eigenvalues satisfy a₁(g) • f = a₁(f) • g.
• HeckeRing.GL2.exists_eq_smul_of_forall_prime_heckeRingHomCusp_of_mem_cuspFormsNew: the same conclusion as proportionality — if one of them is nonzero, the other is a scalar multiple of it.
• HeckeRing.GL2.exists_eq_smul_of_commute_heckeRingHomCusp_of_mem_cuspFormsNew: an endomorphism commuting with the good Hecke operators and preserving the new part acts on such a nonzero eigenvector by a scalar, which is ±1 when the endomorphism squares to the identity on it. This is the common step behind the Fricke and Atkin–Lehner signs of a newform.
• HeckeRing.GL2.cuspFormsNewEigenspace: that simultaneous eigenspace, as a submodule, with HeckeRing.GL2.cuspFormsNewEigenspace_def and HeckeRing.GL2.mem_cuspFormsNewEigenspace_iff.
• HeckeRing.GL2.finrank_cuspFormsNewEigenspace_le_one and HeckeRing.GL2.finrank_cuspFormsNewEigenspace_eq_one: multiplicity one in dimensional form — the eigenspace has dimension at most one, and exactly one once it contains a nonzero form.

References

• T. Miyake, Modular forms, Theorem 4.6.13(1).
• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2.

theorem HeckeRing.GL2.smul_eq_smul_of_forall_prime_heckeRingHomCusp_of_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f g : ↥(cuspFormCharSpace k χ)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) f = c • f ∧ ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) g = c • g) (hf : ↑f ∈ TauCeti.cuspFormsNew N k) (hg : ↑g ∈ TauCeti.cuspFormsNew N k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑g) • ↑f = (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑f) • ↑g

Multiplicity one on the new part of S_k(N, χ) (Miyake, Theorem 4.6.13(1)): two cusp forms in the new part that are eigenvectors of the Hecke ring at every prime not dividing N, with the same eigenvalue at each such prime, are proportional: a₁(g) • f = a₁(f) • g. So each simultaneous eigenspace of the good Hecke operators inside the new part is at most one-dimensional.

theorem HeckeRing.GL2.exists_eq_smul_of_forall_prime_heckeRingHomCusp_of_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f g : ↥(cuspFormCharSpace k χ)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) f = c • f ∧ ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) g = c • g) (hf : ↑f ∈ TauCeti.cuspFormsNew N k) (hg : ↑g ∈ TauCeti.cuspFormsNew N k) (hf0 : ↑f ≠ 0) : ∃ (c : ℂ), ↑g = c • ↑f

Two good Hecke eigenvectors in the new part are proportional, in the form a consumer wants: if f is nonzero, every g sharing its eigenvalues is a scalar multiple of it. So a simultaneous eigenspace of the good Hecke operators inside the new part of S_k(N, χ) is spanned by any one of its nonzero vectors, which is one-dimensionality in concrete form.

The nonvanishing hypothesis is only on f: the case a₁(f) = 0 is not an exception to be excluded but is impossible once f ≠ 0, by eq_zero_of_forall_prime_heckeRingHomCusp_of_one_eq_zero_of_mem_cuspFormsNew.

theorem HeckeRing.GL2.exists_eq_smul_of_commute_heckeRingHomCusp_of_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {W : Module.End ℂ ↥(cuspFormCharSpace k χ)} (hW : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → Commute W ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p))) (hWnew : ∀ (g : ↥(cuspFormCharSpace k χ)), ↑g ∈ TauCeti.cuspFormsNew N k → ↑(W g) ∈ TauCeti.cuspFormsNew N k) {f : ↥(cuspFormCharSpace k χ)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N p)) f = c • f) (hf : ↑f ∈ TauCeti.cuspFormsNew N k) (hf0 : ↑f ≠ 0) (hWW : W (W f) = f) : ∃ (ε : ℂ), (ε = 1 ∨ ε = -1) ∧ W f = ε • f

A commuting involution acts on a good Hecke eigenvector of the new part by a sign. Let W be an endomorphism of S_k(N, χ) commuting with the good Hecke operators Tₚ, p ∤ N, and carrying the new part into itself. A nonzero good Hecke eigenvector f in the new part on which W squares to the identity, W (W f) = f, satisfies W f = ε • f with ε = 1 or ε = -1: W f is a good eigenvector in the new part with the eigenvalues of f, hence a multiple ε • f by multiplicity one, and W (W f) = f forces ε ^ 2 = 1.

Multiplicity one in dimensional form

noncomputable def HeckeRing.GL2.cuspFormsNewEigenspace {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (a : (n : ℕ+) → (↑n).Coprime N → ℂ) : Submodule ℂ ↥(cuspFormCharSpace k χ)

The simultaneous eigenspace of the good Hecke operators in the new part of S_k(N, χ), for the eigenvalue system a: the forms of nebentypus χ lying in S_k(Γ₁(N))ⁿᵉʷ on which Tₙ acts by the scalar a n hn, at every index n coprime to N.

The eigenvalue system is a dependent function of the good index and its coprimality proof, the spelling EigenformAwayFromLevel.eigenvalue uses, so that every value of a is used. The index runs over ℕ+, also as there: at N = 1 the natural number 0 is coprime to N, and T₀ is the identity, so a ℕ-indexed system would impose a spurious constraint at that index.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.GL2.cuspFormsNewEigenspace_def {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (a : (n : ℕ+) → (↑n).Coprime N → ℂ) : cuspFormsNewEigenspace k χ a = (⨅ (n : ℕ+), ⨅ (hn : (↑n).Coprime N), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N ↑n)).eigenspace (a n hn)) ⊓ Submodule.comap (cuspFormCharSpace k χ).subtype (TauCeti.cuspFormsNew N k)

Defining equation for the sealed cuspFormsNewEigenspace: it is the joint eigenspace of the good Hecke operators, met with the new subspace.

@[simp]

theorem HeckeRing.GL2.mem_cuspFormsNewEigenspace_iff {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {a : (n : ℕ+) → (↑n).Coprime N → ℂ} {f : ↥(cuspFormCharSpace k χ)} : f ∈ cuspFormsNewEigenspace k χ a ↔ (∀ (n : ℕ+) (hn : (↑n).Coprime N), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N ↑n)) f = a n hn • f) ∧ ↑f ∈ TauCeti.cuspFormsNew N k

Membership in the simultaneous eigenspace: the good eigenvector equations together with newness.

theorem HeckeRing.GL2.cuspFormsNewEigenspace_le_span_singleton {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {a : (n : ℕ+) → (↑n).Coprime N → ℂ} {f : ↥(cuspFormCharSpace k χ)} (hf : f ∈ cuspFormsNewEigenspace k χ a) (hf0 : f ≠ 0) : cuspFormsNewEigenspace k χ a ≤ ℂ ∙ f

The simultaneous eigenspace is spanned by any one of its nonzero forms. This is exists_eq_smul_of_forall_prime_heckeRingHomCusp_of_mem_cuspFormsNew read as a statement about the eigenspace rather than about a pair of forms.

theorem HeckeRing.GL2.finrank_cuspFormsNewEigenspace_le_one {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (a : (n : ℕ+) → (↑n).Coprime N → ℂ) : Module.finrank ℂ ↥(cuspFormsNewEigenspace k χ a) ≤ 1

Multiplicity one, in dimensional form (Miyake, Theorem 4.6.13(1)): a simultaneous eigenspace of the good Hecke operators inside S_k(N, χ)ⁿᵉʷ has dimension at most one.

theorem HeckeRing.GL2.finrank_cuspFormsNewEigenspace_eq_one {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {a : (n : ℕ+) → (↑n).Coprime N → ℂ} {f : ↥(cuspFormCharSpace k χ)} (hf : f ∈ cuspFormsNewEigenspace k χ a) (hf0 : f ≠ 0) : Module.finrank ℂ ↥(cuspFormsNewEigenspace k χ a) = 1

Multiplicity one, in dimensional form: once a simultaneous eigenspace of the good Hecke operators inside S_k(N, χ)ⁿᵉʷ contains a nonzero form, it is a line.