The newforms are an orthogonal basis of the new subspace #

The newforms of level N and weight k form a Petersson-orthogonal basis of the new subspace S_k(Γ₁(N))ⁿᵉʷ, and those of nebentypus χ span its χ-part S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ).

Orthogonality. Good Hecke eigenforms whose eigenvalues differ at a prime p ∤ N are orthogonal (HeckeRing.GL2.EigenformAwayFromLevel.peterssonInnerCosets_eq_zero_of_eigenvalue_ne, from the Petersson adjoint of Tₚ). Two distinct newforms differ in nebentypus or at some good prime, since a newform is determined by its nebentypus and its eigenvalues at the good primes.

Spanning. S_k(N, χ) has a basis of good Hecke eigenforms, and its old and new parts are stable under the good Tₚ and complementary. So the new part of each basis vector is again a good Hecke eigenvector, and these new parts span S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ). A nonzero good Hecke eigenvector in the new subspace has a₁ ≠ 0, so dividing by a₁ makes it a newform.

Main definitions #

HeckeRing.GL2.Newform.ofForallPrime: a nonzero cusp form of nebentypus χ in the new subspace that is an eigenvector of every good Tₚ, divided by its first coefficient, as a newform.
HeckeRing.GL2.Newform.basis: the newforms, as a basis of S_k(Γ₁(N))ⁿᵉʷ.

Main results #

HeckeRing.GL2.Newform.peterssonInnerCosets_eq_zero_of_ne: distinct newforms are orthogonal.
HeckeRing.GL2.Newform.span_image_toCuspForm_eq_cuspFormsNew_inf_cuspFormCharSpace: the newforms of nebentypus χ span S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ).
HeckeRing.GL2.Newform.span_range_toCuspForm_eq_cuspFormsNew: the newforms span S_k(Γ₁(N))ⁿᵉʷ.
HeckeRing.GL2.Newform.linearIndependent_toCuspForm: the newforms are linearly independent.

References #

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

Orthogonality #

source

theorem HeckeRing.GL2.Newform.peterssonInnerCosets_eq_zero_of_ne {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} (h : f ≠ g) :

f.peterssonInnerCosets g.toCuspForm = 0

Distinct newforms are orthogonal: the Petersson product of two distinct newforms of level N and weight k, of the same or of different nebentypus, vanishes.

source

theorem HeckeRing.GL2.Newform.linearIndependent_toCuspForm {N : ℕ} [NeZero N] {k : ℤ} :

LinearIndependent ℂ fun (f : Newform N k) => f.toCuspForm

The newforms are linearly independent: the underlying cusp forms of the newforms of level N and weight k are linearly independent.

Normalising a new eigenvector #

source

noncomputable def HeckeRing.GL2.Newform.ofForallPrime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂ ˣ} {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : F ∈ cuspFormCharSpace k χ) (hnew : F ∈ TauCeti.cuspFormsNew N k) (hF : F ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨F, hχ⟩ = c • ⟨F, hχ⟩) :

Newform N k

A new eigenvector, normalised, is a newform. A nonzero cusp form of nebentypus χ in the new subspace that is an eigenvector of the Hecke ring at every prime not dividing N, divided by its first coefficient (which is nonzero).

Equations

HeckeRing.GL2.Newform.ofForallPrime hχ hnew hF h = { toEigenformAwayFromLevel := HeckeRing.GL2.EigenformAwayFromLevel.ofForallPrime ⋯ ⋯ ⋯, isNew := ⋯, isNorm := ⋯ }

Instances For

source

@[simp]

theorem HeckeRing.GL2.Newform.ofForallPrime_toCuspForm {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂ ˣ} {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : F ∈ cuspFormCharSpace k χ) (hnew : F ∈ TauCeti.cuspFormsNew N k) (hF : F ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨F, hχ⟩ = c • ⟨F, hχ⟩) :

(ofForallPrime hχ hnew hF h).toCuspForm = ((PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑F))⁻¹ • F

The underlying cusp form of ofForallPrime is the supplied form divided by its first coefficient.

source

@[simp]

theorem HeckeRing.GL2.Newform.ofForallPrime_χ {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂ ˣ} {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : F ∈ cuspFormCharSpace k χ) (hnew : F ∈ TauCeti.cuspFormsNew N k) (hF : F ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨F, hχ⟩ = c • ⟨F, hχ⟩) :

(ofForallPrime hχ hnew hF h).χ = χ

The nebentypus of ofForallPrime is the character supplied to the constructor.

Spanning #

source

theorem HeckeRing.GL2.Newform.span_image_toCuspForm_eq_cuspFormsNew_inf_cuspFormCharSpace {N : ℕ} [NeZero N] {k : ℤ} (χ : (ZMod N)ˣ →* ℂ ˣ) :

Submodule.span ℂ ((fun (f : Newform N k) => f.toCuspForm) '' {f : Newform N k | f.χ = χ}) = TauCeti.cuspFormsNew N k ⊓ cuspFormCharSpace k χ

The newforms of nebentypus χ span the new part of S_k(N, χ) (Miyake, Theorem 4.6.13(2)): the span of their underlying cusp forms is S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ).

source

theorem HeckeRing.GL2.Newform.span_range_toCuspForm_eq_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} :

Submodule.span ℂ (Set.range fun (f : Newform N k) => f.toCuspForm) = TauCeti.cuspFormsNew N k

The newforms span the new subspace: the span of the underlying cusp forms of the newforms of level N and weight k is S_k(Γ₁(N))ⁿᵉʷ.

The basis #

source

noncomputable def HeckeRing.GL2.Newform.basis (N : ℕ) [NeZero N] (k : ℤ) :

Module.Basis (Newform N k) ℂ ↥(TauCeti.cuspFormsNew N k)

The newforms, as a basis of the new subspace S_k(Γ₁(N))ⁿᵉʷ (Miyake, Theorem 4.6.13(2); Diamond–Shurman, Theorem 5.8.2). It is Petersson-orthogonal: Newform.peterssonInnerCosets_eq_zero_of_ne.

Equations