The Atkin–Lehner operators preserve the old subspace

Let Q ∥ N be an exact divisor and W_Q an Atkin–Lehner matrix of level N for Q. By TauCeti/NumberTheory/ModularForms/AtkinLehner/LevelRaise.lean, W_Q intertwines a level-raise V_d from a divisor level M with a level-raise V_e from M, at the cost of replacing W_Q by an Atkin–Lehner operator W_{Q₁} of level M:

W_Q (V_d f) = d₁⁻¹ · e₁ ^ (k - 1) · V_e (W_{Q₁} f).

The Atkin–Lehner operators live on S_k(Γ₀(N)), while the old subspace S_k(Γ₁(N))ᵒˡᵈ is spanned by level-raises of forms on Γ₁(M). The two are matched through the trace from Γ₁(N) to Γ₀(N), which is the sum of the diamond operators (TauCeti.cuspFormTraceGamma0): it carries V_d g to V_d of the diamond sum of g, a form of trivial nebentypus, hence a form on Γ₀(M); and it multiplies a form on Γ₀(N) by #(ZMod N)ˣ. Since the old subspace is generated by the degeneracy maps V₁, V_p from the levels N / p (TauCeti.cuspFormsOld_le_of_prime), the intertwining identity then shows that W_Q preserves oldness of forms on Γ₀(N). Combined with the Petersson self-adjointness of the normalized operator 𝒲_Q (TauCeti/NumberTheory/ModularForms/Petersson/AtkinLehner.lean), this is what makes the new subspace of trivial nebentypus stable under 𝒲_Q, the input to the Atkin–Lehner signs of newforms.

Main results

• TauCeti.Nat.IsExactDivisor.ofLe_atkinLehnerOperatorCusp_mem_cuspFormsOld, TauCeti.Nat.IsExactDivisor.ofLe_normalizedAtkinLehnerOperatorCusp_mem_cuspFormsOld: for a cusp form on Γ₀(N) that is old at level Γ₁(N), its image under W_Q (resp. 𝒲_Q) is again old.

References

• A. O. L. Atkin and J. Lehner, Hecke operators on Γ₀(m), Math. Ann. 185 (1970), 134–160.
• F. Diamond and J. Shurman, A First Course in Modular Forms, §5.6 and §5.10.
• Miyake, Modular forms, Section 4.6.

Stability of the old subspace at trivial nebentypus

theorem TauCeti.Nat.IsExactDivisor.ofLe_atkinLehnerOperatorCusp_mem_cuspFormsOld {N Q : ℕ} {k : ℤ} [NeZero N] (h : IsExactDivisor Q N) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k} (hf : CuspForm.ofLe ⋯ f ∈ cuspFormsOld N k) : CuspForm.ofLe ⋯ ((h.atkinLehnerOperatorCusp k) f) ∈ cuspFormsOld N k

The Atkin–Lehner operator preserves the old subspace at trivial nebentypus. For a cusp form f on Γ₀(N) whose restriction to Γ₁(N) is old, the restriction of W_Q f is again old, for every exact divisor Q ∥ N.

theorem TauCeti.Nat.IsExactDivisor.ofLe_normalizedAtkinLehnerOperatorCusp_mem_cuspFormsOld {N Q : ℕ} {k : ℤ} [NeZero N] (h : IsExactDivisor Q N) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k} (hf : CuspForm.ofLe ⋯ f ∈ cuspFormsOld N k) : CuspForm.ofLe ⋯ ((h.normalizedAtkinLehnerOperatorCusp k) f) ∈ cuspFormsOld N k

The normalized Atkin–Lehner operator preserves the old subspace at trivial nebentypus. For a cusp form f on Γ₀(N) whose restriction to Γ₁(N) is old, the restriction of 𝒲_Q f is again old, 𝒲_Q being a scalar multiple of W_Q.