The old and new subspaces at a prime

Fix a prime q dividing the level N. The q-old subspace S_k(Γ₁(N))^{q-old} is spanned by the level-raises V_d f of the forms f of the levels M whose q-adic valuation is smaller than that of N, that is with q * M ∣ N; it is generated by the two degeneracy maps V₁, V_q : S_k(Γ₁(N / q)) → S_k(Γ₁(N)). The q-new subspace is its Petersson-orthogonal complement. Every oldform from a level with smaller q-part is q-old, so the q-old subspace lies in the old subspace and every newform is q-new.

The point of the q-new subspace is that it is stable under the level-raises V_d that do not raise the q-adic valuation of the level: if G is q-new of level K, d * K ∣ K' and q * K ∤ K', then V_d G is q-new of level K' (TauCeti.levelRaise_mem_cuspFormsNewAt). This is what separates two newforms of levels with different q-parts when they are compared at a common level, the step behind strong multiplicity one across unrelated levels.

Main definitions

• TauCeti.cuspFormsOldAt N k q: the q-old subspace of S_k(Γ₁(N)); TauCeti.cuspFormsOldAt_def identifies it with cuspFormsOldOf for the condition q * M ∣ N.
• TauCeti.cuspFormsNewAt N k q: the q-new subspace, its Petersson-orthogonal complement; TauCeti.mem_cuspFormsNewAt_iff tests it on the level-raises.

Main results

• TauCeti.levelRaise_mem_cuspFormsOldAt and TauCeti.cuspFormsOldAt_le: the introduction and elimination rules of the q-old subspace; TauCeti.cuspFormsOldAt_le_of_prime is the elimination rule through the two degeneracy maps from level N / q.
• TauCeti.cuspFormsOldAt_le_cuspFormsOld, TauCeti.cuspFormsNew_le_cuspFormsNewAt: q-old forms are old, and newforms are q-new; TauCeti.cuspFormsNewAt_eq_top: for q ∤ N every form is q-new.
• TauCeti.levelRaise_mem_cuspFormsOldAt_of_mem: V_d carries q-old forms to q-old forms.
• TauCeti.frickeOperatorCusp_mem_cuspFormsNewAt_iff: the Fricke involution preserves the q-new subspace.
• TauCeti.peterssonInnerCosets_levelRaise_eq_zero_iff: ⟪V_q φ, H⟫ vanishes exactly when the pairing of φ with H ∣ diag(q, 1)⁻¹ on diag(q, 1) Γ₁(N) diag(q, 1)⁻¹ does.
• TauCeti.restrict_mem_cuspFormsNewAt, TauCeti.levelRaise_mem_cuspFormsNewAt: restriction to a level with the same q-part, and more generally V_d with q * K ∤ K', preserve q-newness.

References

• A. O. L. Atkin and J. Lehner, Hecke operators on Γ₀(m), Math. Ann. 185 (1970), 134–160.
• W.-C. W. Li, Newforms and functional equations, Math. Ann. 212 (1975), 285–315.
• T. Miyake, Modular forms, Section 4.6.
• F. Diamond and J. Shurman, A first course in modular forms, Section 5.6.

The q-old subspace

noncomputable def TauCeti.cuspFormsOldAt (N : ℕ) [NeZero N] (k : ℤ) (q : ℕ) : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The q-old subspace of S_k(Γ₁(N)): the span of the level-raises V_d : S_k(Γ₁(M)) → S_k(Γ₁(N)) over the pairs (M, d) with d * M ∣ N and q * M ∣ N, that is from the levels M whose q-part is a proper divisor of that of N, that is cuspFormsOldOf for the condition q * M ∣ N. For a prime q ∣ N it is generated by the two degeneracy maps from level N / q (cuspFormsOldAt_le_of_prime).

theorem TauCeti.cuspFormsOldAt_def (N : ℕ) [NeZero N] (k : ℤ) (q : ℕ) : cuspFormsOldAt N k q = cuspFormsOldOf N k fun (x : ℕ) => q * x ∣ N

Defining equation for the sealed cuspFormsOldAt: it is cuspFormsOldOf for the levels M with q * M ∣ N.

theorem TauCeti.levelRaise_mem_cuspFormsOldAt {M d N q : ℕ} [NeZero N] (h : d * M ∣ N) (hq : q * M ∣ N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : CuspForm.levelRaise d ⋯ f ∈ cuspFormsOldAt N k q

Introduction rule for the q-old subspace: a level-raise from a level M with q * M ∣ N is q-old.

theorem TauCeti.cuspFormsOldAt_le {k : ℤ} {N q : ℕ} [NeZero N] {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (hV : ∀ (M d : ℕ) (h : d * M ∣ N), q * M ∣ N → ∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k), CuspForm.levelRaise d ⋯ f ∈ V) : cuspFormsOldAt N k q ≤ V

Elimination rule for the q-old subspace: a subspace containing every level-raise from a level M with q * M ∣ N contains the q-old subspace.

theorem TauCeti.cuspFormsOldAt_le_of_prime {k : ℤ} {N q : ℕ} [NeZero N] {L : ℕ} (hq : Nat.Prime q) (hL : q * L = N) {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (h₁ : ∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 L)) k), CuspForm.restrict ⋯ f ∈ V) (h₂ : ∀ (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 L)) k), CuspForm.levelRaise q ⋯ f ∈ V) : cuspFormsOldAt N k q ≤ V

The q-old subspace is generated by the two degeneracy maps from level N / q. For a prime q and q * L = N, a subspace containing the restrictions V₁ f and the level-raises V_q f of the forms f of level L contains the q-old subspace.

theorem TauCeti.cuspFormsOldAt_le_cuspFormsOld {k : ℤ} {N q : ℕ} [NeZero N] (hq : q ≠ 1) : cuspFormsOldAt N k q ≤ cuspFormsOld N k

q-old forms are old: for q ≠ 1, a level M with q * M ∣ N is a proper divisor of N.

theorem TauCeti.levelRaise_mem_cuspFormsOldAt_of_mem {k : ℤ} {d q K K' : ℕ} [NeZero K] [NeZero K'] [NeZero d] (hdK : d * K ∣ K') {G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 K)) k} (hG : G ∈ cuspFormsOldAt K k q) : CuspForm.levelRaise d ⋯ G ∈ cuspFormsOldAt K' k q

V_d carries q-old forms to q-old forms: if d * K ∣ K', then V_d maps S_k(Γ₁(K))^{q-old} into S_k(Γ₁(K'))^{q-old}, since V_d ∘ V_e = V_{e d}.

The q-new subspace

noncomputable def TauCeti.cuspFormsNewAt (N : ℕ) [NeZero N] (k : ℤ) (q : ℕ) : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The q-new subspace of S_k(Γ₁(N)): the Petersson-orthogonal complement of the q-old subspace.

theorem TauCeti.cuspFormsNewAt_def (N : ℕ) [NeZero N] (k : ℤ) (q : ℕ) : cuspFormsNewAt N k q = CuspForm.peterssonOrthogonal (cuspFormsOldAt N k q)

Defining equation for cuspFormsNewAt: it is the Petersson-orthogonal complement of the q-old subspace.

@[simp]

theorem TauCeti.mem_cuspFormsNewAt_iff {k : ℤ} {N q : ℕ} [NeZero N] {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} : f ∈ cuspFormsNewAt N k q ↔ ∀ (M d : ℕ) (h : d * M ∣ N), q * M ∣ N → ∀ (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k), (CuspForm.levelRaise d ⋯ g).peterssonInnerCosets f = 0

q-newness is tested on the level-raises. A cusp form of level N is q-new exactly when it is Petersson-orthogonal to V_d g for every cusp form g of a level M with q * M ∣ N.

theorem TauCeti.isCompl_cuspFormsOldAt_cuspFormsNewAt (N : ℕ) [NeZero N] (k : ℤ) (q : ℕ) : IsCompl (cuspFormsOldAt N k q) (cuspFormsNewAt N k q)

The q-old and q-new subspaces are complements, so every cusp form splits uniquely as a q-old form plus a q-new form.

theorem TauCeti.cuspFormsNew_le_cuspFormsNewAt {k : ℤ} {N q : ℕ} [NeZero N] (hq : q ≠ 1) : cuspFormsNew N k ≤ cuspFormsNewAt N k q

Newforms are q-new: for q ≠ 1 the q-old subspace lies in the old subspace, so its orthogonal complement contains the new subspace.

@[simp]

theorem TauCeti.cuspFormsOldAt_eq_bot {k : ℤ} {N q : ℕ} [NeZero N] (hqN : ¬q ∣ N) : cuspFormsOldAt N k q = ⊥

Away from the level there are no q-old forms: if q ∤ N, no level M has q * M ∣ N.

@[simp]

theorem TauCeti.cuspFormsNewAt_eq_top {k : ℤ} {N q : ℕ} [NeZero N] (hqN : ¬q ∣ N) : cuspFormsNewAt N k q = ⊤

Away from the level every form is q-new.

theorem TauCeti.restrict_mem_cuspFormsOldAt {M N q : ℕ} [NeZero N] (hq : q * M ∣ N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : CuspForm.restrict ⋯ f ∈ cuspFormsOldAt N k q

Restriction from a level M with q * M ∣ N is q-old: it is the level-raise V₁.

The Fricke involution

theorem TauCeti.frickeOperatorCusp_mem_cuspFormsNewAt_iff {k : ℤ} {N q : ℕ} [NeZero N] {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} : (frickeOperatorCusp k) f ∈ cuspFormsNewAt N k q ↔ f ∈ cuspFormsNewAt N k q

The Fricke operator preserves the q-new subspace, in both directions.

Conjugating the pairing by diag(q, 1)

theorem TauCeti.peterssonInnerCosets_levelRaise_eq_zero_iff {k : ℤ} {M N q : ℕ} [NeZero q] [NeZero N] {hqM : q * M ∣ N} {φ : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k} {H : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} : (CuspForm.levelRaise q ⋯ φ).peterssonInnerCosets H = 0 ↔ (CuspForm.restrict ⋯ φ).peterssonInnerCosets (CuspForm.restrict ⋯ (CuspForm.translate H (scaleGL q)⁻¹)) = 0

⟪V_q φ, H⟫ vanishes exactly when its diag(q, 1)-conjugate does: the pairing on Γ₁(N) of V_q φ with H vanishes exactly when the pairing on diag(q, 1) Γ₁(N) diag(q, 1)⁻¹ of φ with H ∣ diag(q, 1)⁻¹ does.

Restriction preserves q-newness

theorem TauCeti.restrict_mem_cuspFormsNewAt {k : ℤ} {q K K' : ℕ} [NeZero K] [NeZero K'] (hq : Nat.Prime q) (hKK' : K ∣ K') (hqKK' : ¬q * K ∣ K') {G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 K)) k} (hG : G ∈ cuspFormsNewAt K k q) : CuspForm.restrict ⋯ G ∈ cuspFormsNewAt K' k q

Restriction to a level with the same q-part preserves q-newness. If q is a prime, K ∣ K' and q * K ∤ K', the restriction to Γ₁(K') of a q-new form of level K is q-new.

theorem TauCeti.levelRaise_mem_cuspFormsNewAt {k : ℤ} {d q K K' : ℕ} [NeZero K] [NeZero K'] [NeZero d] (hq : Nat.Prime q) (hdK : d * K ∣ K') (hqKK' : ¬q * K ∣ K') {G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 K)) k} (hG : G ∈ cuspFormsNewAt K k q) : CuspForm.levelRaise d ⋯ G ∈ cuspFormsNewAt K' k q

V_d preserves q-newness when it does not raise the q-part of the level. If q is a prime, d * K ∣ K' and q * K ∤ K' (so q ∤ d), then V_d carries S_k(Γ₁(K))^{q-new} into S_k(Γ₁(K'))^{q-new}.