The old and new subspaces of S_k(Γ₁(N))

A cusp form of level M produces cusp forms of level N for every multiple N of M: if d * M ∣ N then the level-raising operator V_d, (V_d f)(τ) = f(dτ) of TauCeti.CuspForm.levelRaise, carries S_k(Γ₁(M)) into S_k(Γ₁(N)). The old subspace S_k(Γ₁(N))ᵒˡᵈ is the span of all of these images with M a proper divisor of N, and the new subspace S_k(Γ₁(N))ⁿᵉʷ is its Petersson-orthogonal complement.

The properness condition is imposed as M ≠ N, which discards exactly one pair: d * M ∣ N already forces d = 1 when M = N, so the only excluded operator is the identity V₁ at the level itself. Every other pair contributes, including M ∣ N proper with d = 1, the plain restriction of a lower-level form (ofLe_mem_cuspFormsOld).

The old subspace is stable under the diamond operators, because V_d intertwines them: ⟨u⟩ at level N acts on V_d f as ⟨u mod M⟩ acts on f (TauCeti.CuspForm.diamondOpCusp_levelRaise). This is the lemma behind the fixed-nebentypus refinement S_k(N, χ)ⁿᵉʷ = S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ) of Layer 3 of the ModularForms roadmap, which additionally needs the diamond operators to be Petersson-unitary and is carried out in TauCeti/NumberTheory/ModularForms/Newforms/Nebentypus.lean.

The old subspace is likewise stable under the Hecke operators Tₚ at every prime p (TauCeti.heckeTCuspNat_mem_cuspFormsOld, in TauCeti/NumberTheory/ModularForms/Newforms/Hecke/Stability.lean), for the Hecke action HeckeRing.GL2.heckeTCuspNat on cusp forms. The same file proves the stability of the new subspace at primes coprime to the level.

Main definitions

• TauCeti.cuspFormsOld: the old subspace S_k(Γ₁(N))ᵒˡᵈ.
• TauCeti.cuspFormsNew: the new subspace S_k(Γ₁(N))ⁿᵉʷ, the Petersson-orthogonal complement of the old one.
• TauCeti.cuspFormsOldMultiples: the part of the old subspace generated by the new forms at proper divisor levels that are multiples of a given m. No nebentypus condition is imposed on the generators, so this is an uncharactered auxiliary space.

Main results

• TauCeti.levelRaise_mem_cuspFormsOld and TauCeti.cuspFormsOld_le: the introduction and elimination rules for the old subspace.
• TauCeti.levelRaise_mem_cuspFormsOldMultiples and TauCeti.cuspFormsOldMultiples_le: the introduction and elimination rules for the refined old subspace.
• TauCeti.cuspFormsOldMultiples_le_cuspFormsOld and TauCeti.cuspFormsOldMultiples_le_of_dvd: the refined old subspace sits inside the old subspace, and shrinks as the level condition tightens.
• TauCeti.cuspFormsOldMultiples_one_eq_cuspFormsOld: the old subspace is generated by the level-raised new subspaces of the proper divisor levels.
• TauCeti.cuspFormsOld_le_of_prime: the sharper elimination rule of Diamond–Shurman, in which only the two degeneracy maps S_k(Γ₁(N/p)) → S_k(Γ₁(N)) at each prime p ∣ N are tested.
• TauCeti.mem_cuspFormsNew_iff: a form is new exactly when it is Petersson-orthogonal to every level-raised form from a proper divisor level.
• TauCeti.disjoint_cuspFormsOld_cuspFormsNew: the two subspaces meet only in 0.
• TauCeti.sup_cuspFormsOld_cuspFormsNew_eq_top: the old and new subspaces span the full cusp-form space.
• TauCeti.isCompl_cuspFormsOld_cuspFormsNew: the two subspaces are complements, so every cusp form splits uniquely as an oldform plus a newform. The splitting map is Mathlib's Submodule.projection at this witness, which carries the reconstruction equation and the characterisations of its fixed points and kernel.
• TauCeti.CuspForm.diamondOpCusp_levelRaise: V_d intertwines the diamond operators, whence TauCeti.diamondOpCusp_mem_cuspFormsOld, the diamond stability of the old subspace.
• TauCeti.cuspFormsOld_one, TauCeti.cuspFormsNew_one: at level one there are no oldforms, so every cusp form is new.

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 5.6.
• Miyake, Modular forms, Section 4.6.
• AINTLIB's LeanModularForms/HeckeRIngs/GL2/Newforms/Basic.lean, by the LeanModularForms contributors (Apache-2.0), pinned at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, for the cuspFormsOld and cuspFormsNew API and for the IsCompl statement of the old/new decomposition at lines 293-400. The IsCompl proof is not adapted from there — that source derives it through a real bilinear form, whereas here it is assembled from CuspForm.isCompl_peterssonOrthogonal.

The old subspace

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

The old subspace S_k(Γ₁(N))ᵒˡᵈ: the subspace of S_k(Γ₁(N)) spanned by the images of the level-raising operators V_d : S_k(Γ₁(M)) → S_k(Γ₁(N)) over all pairs (M, d) with d * M ∣ N and M a proper divisor of N. Since d * M ∣ N forces d = 1 when M = N, the condition M ≠ N removes exactly the identity operator at level N.

Equations

• TauCeti.cuspFormsOld N k = ⨆ (M : ℕ), ⨆ (d : ℕ), ⨆ (h : d * M ∣ N ∧ M ≠ N), have this := ⋯; (TauCeti.CuspForm.levelRaiseₗ d ⋯).range

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

Introduction rule for the old subspace: every level-raise from a proper divisor level is old.

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

Elimination rule for the old subspace: a subspace containing every level-raise from a proper divisor level contains the whole old subspace.

theorem TauCeti.ofLe_mem_cuspFormsOld {M N : ℕ} [NeZero N] (h : M ∣ N) (hM : M ≠ N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : CuspForm.ofLe ⋯ f ∈ cuspFormsOld N k

The restriction to level N of a cusp form of proper divisor level M is old: it is the level-raise V₁.

@[simp]

theorem TauCeti.cuspFormsOld_one (k : ℤ) : cuspFormsOld 1 k = ⊥

Level one has no oldforms: 1 has no proper divisors.

theorem TauCeti.cuspFormsOld_le_of_prime {k : ℤ} {N : ℕ} [NeZero N] {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (hV : ∀ (p L : ℕ), Nat.Prime p → ∀ (hpL : p * L = N) (d : ℕ) (hd : d = 1 ∨ d = p) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 L)) k), have hdvd := ⋯; CuspForm.levelRaise d ⋯ g ∈ V) : cuspFormsOld N k ≤ V

The old subspace is generated by the prime-level degeneracy maps. Every level-raise V_d f from a proper divisor level factors through an intermediate level L with p * L = N for a prime p, the last step being V₁ or V_p. So the definition above, a supremum over all proper divisor levels, agrees with Diamond–Shurman's presentation of the old subspace by the two degeneracy maps S_k(Γ₁(N/p)) → S_k(Γ₁(N)) attached to each prime p ∣ N: a subspace closed under those already contains every oldform.

The factorization is V_d = V_p ∘ V_{d/p} when a prime p divides d, and V₁ = V₁ ∘ V₁ through the level N/p for a prime p dividing N/M otherwise.

The new subspace

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

The new subspace S_k(Γ₁(N))ⁿᵉʷ: the Petersson-orthogonal complement of the old subspace inside S_k(Γ₁(N)).

Equations

• TauCeti.cuspFormsNew N k = TauCeti.CuspForm.peterssonOrthogonal (TauCeti.cuspFormsOld N k)

theorem TauCeti.cuspFormsNew_def (N : ℕ) [NeZero N] (k : ℤ) : cuspFormsNew N k = CuspForm.peterssonOrthogonal (cuspFormsOld N k)

Defining equation for the sealed cuspFormsNew: it is the Petersson-orthogonal complement of the old subspace.

@[simp]

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

Newness is tested on the level-raises. A cusp form of level N is new exactly when it is Petersson-orthogonal to V_d g for every cusp form g of proper divisor level.

theorem TauCeti.disjoint_cuspFormsOld_cuspFormsNew (N : ℕ) [NeZero N] (k : ℤ) : Disjoint (cuspFormsOld N k) (cuspFormsNew N k)

The old and new subspaces meet only in 0, by positive definiteness of the Petersson product.

theorem TauCeti.sup_cuspFormsOld_cuspFormsNew_eq_top (N : ℕ) [NeZero N] (k : ℤ) : cuspFormsOld N k ⊔ cuspFormsNew N k = ⊤

The old and new subspaces span the full cusp-form space.

@[simp]

theorem TauCeti.cuspFormsNew_one (k : ℤ) : cuspFormsNew 1 k = ⊤

At level one every cusp form is new, there being no oldforms to be orthogonal to.

The old/new decomposition

theorem TauCeti.isCompl_cuspFormsOld_cuspFormsNew (N : ℕ) [NeZero N] (k : ℤ) : IsCompl (cuspFormsOld N k) (cuspFormsNew N k)

The old and new subspaces are complements. Diamond–Shurman (5.20): S_k(Γ₁(N)) = S_k(Γ₁(N))ᵒˡᵈ ⊕ S_k(Γ₁(N))ⁿᵉʷ.

The old subspace generated by newforms at prescribed levels

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

The part of the old subspace generated by the new forms at proper divisor levels that are multiples of m: the supremum of the V_d-images of S_k(Γ₁(M))ⁿᵉʷ over the pairs (M, d) with d * M ∣ N, M ≠ N and m ∣ M.

The intended m is the conductor of a nebentypus character, which is why the level condition is divisibility by m; but this is not Miyake's S_k^♭(N, χ) (p. 162). The generators here range over the whole newspace cuspFormsNew M k at each eligible level, including forms of nebentypus unrelated to χ, whereas Miyake's space is generated by the χ-isotypic newspaces together with the character transition along each M ∣ N. Recovering S_k^♭(N, χ) needs those. This is an uncharactered auxiliary subspace of the old subspace — neither containing nor contained in Miyake's space in general — and it is what the inclusion into cuspFormsOld below is stated for.

Equations

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

theorem TauCeti.levelRaise_mem_cuspFormsOldMultiples {M d N : ℕ} [NeZero N] {m : ℕ} (h : d * M ∣ N) (hM : M ≠ N) (hm : m ∣ M) (k : ℤ) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) (hg : g ∈ cuspFormsNew M k) : (CuspForm.levelRaiseₗ d ⋯) g ∈ cuspFormsOldMultiples N k m

Introduction rule: a newform at a proper divisor level divisible by m, level-raised, lies in cuspFormsOldMultiples.

theorem TauCeti.cuspFormsOldMultiples_le_cuspFormsOld (N : ℕ) [NeZero N] (k : ℤ) (m : ℕ) : cuspFormsOldMultiples N k m ≤ cuspFormsOld N k

Newforms level-raised from proper divisor levels are old, whatever the level condition m ∣ M selects. Only d * M ∣ N and M ≠ N are used — the newness of the raised form and the divisibility by m are both discarded, which is why one inclusion is elementary while the reverse is not.

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

Elimination rule for the refined old subspace: a subspace containing every level-raise of a newform from a proper divisor level divisible by m contains the whole refined old subspace.

This is the companion to levelRaise_mem_cuspFormsOldMultiples, and it is what downstream proofs use rather than the lattice lemmas directly.

theorem TauCeti.cuspFormsOldMultiples_le_of_dvd (N : ℕ) [NeZero N] (k : ℤ) {m m' : ℕ} (h : m' ∣ m) : cuspFormsOldMultiples N k m ≤ cuspFormsOldMultiples N k m'

cuspFormsOldMultiples is monotone in the level condition: a coarser divisibility requirement admits more generators.

theorem TauCeti.cuspFormsOldMultiples_one_eq_cuspFormsOld (N : ℕ) [NeZero N] (k : ℤ) : cuspFormsOldMultiples N k 1 = cuspFormsOld N k

The old subspace is generated by the level-raised new subspaces: every oldform of level Γ₁(N) is a combination of forms V_d g with g new of a proper divisor level M and d * M ∣ N. With sup_cuspFormsOld_cuspFormsNew_eq_top this is the spanning half of Diamond–Shurman, Theorem 5.8.3.

Diamond stability of the old subspace

theorem TauCeti.diamondOpCusp_mem_cuspFormsOld {k : ℤ} {N : ℕ} [NeZero N] (u : (ZMod N)ˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOld N k) : (diamondOpCusp k u) f ∈ cuspFormsOld N k

The old subspace is diamond-stable.

theorem TauCeti.cuspFormsOld_map_diamondOpCusp_le {N : ℕ} [NeZero N] (u : (ZMod N)ˣ) (k : ℤ) : Submodule.map (diamondOpCusp k u) (cuspFormsOld N k) ≤ cuspFormsOld N k

The old subspace is diamond-stable, in the Submodule.map form.