The cusp--Eisenstein decomposition for congruence subgroups

Let Γ be a subgroup of SL(2, ℤ) containing the principal congruence subgroup Γ(N), such as Γ₁(N) (via CongruenceSubgroup.Gamma_le_Gamma1) or Γ₀(N). In weight at least three, the Eisenstein subspace for Γ is the space of forms whose restriction to Γ(N) belongs to the span of the primitive residue-class Eisenstein series. This file proves that it is complementary to the cusp forms.

The decomposition descends from the corresponding decomposition for Γ(N) by ModularForm.isCompl_comap_restrictₗ_cuspFormSubmodule, since the primitive Eisenstein span is stable under slashing by SL(2, ℤ): the slash transformation formula sends the series with residue a to the series whose residue is the right translate of a.

Main results

• TauCeti.EisensteinSeries.gammaSlashₗ_eisensteinSeriesMF: integral slash operators permute the primitive residue-class Eisenstein generators.
• TauCeti.EisensteinSeries.congruenceEisensteinSubspace: the Eisenstein subspace of M_k(Γ) detected after restriction to Γ(N).
• TauCeti.EisensteinSeries.isCompl_congruenceEisensteinSubspace_cuspFormSubmodule: the cusp--Eisenstein decomposition of M_k(Γ) in weight at least three.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, Section 4.2.

theorem TauCeti.EisensteinSeries.eisensteinSeries_slash_mapGL {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (eisensteinSeries a k) = eisensteinSeries (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k

Slashing a primitive residue-class Eisenstein series by an integral determinant-one matrix permutes its residue class, with the matrix viewed in the real general linear group.

theorem TauCeti.EisensteinSeries.gammaSlashₗ_eisensteinSeriesMF {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.gammaSlashₗ γ) (ModularForm.eisensteinSeriesMF hk a) = ModularForm.eisensteinSeriesMF hk (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

The principal-level slash operator sends a bundled primitive Eisenstein generator to the generator with right-translated residue.

theorem TauCeti.EisensteinSeries.gammaSlashₗ_mem_primitiveEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k} (hf : f ∈ primitiveEisensteinSubspace N hk) : (ModularForm.gammaSlashₗ γ) f ∈ primitiveEisensteinSubspace N hk

The primitive Eisenstein span of M_k(Γ(N)) is stable under slashing by SL(2, ℤ).

noncomputable def TauCeti.EisensteinSeries.congruenceEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The Eisenstein subspace of M_k(Γ), for a subgroup Γ of SL(2, ℤ) containing Γ(N), in weight at least three: a form belongs to it exactly when its restriction to Γ(N) belongs to the primitive residue-class Eisenstein span.

theorem TauCeti.EisensteinSeries.congruenceEisensteinSubspace_def {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : congruenceEisensteinSubspace hΓ hk = Submodule.comap (ModularForm.restrictₗ k ℂ ⋯) (primitiveEisensteinSubspace N hk)

The defining pullback of the primitive Eisenstein span along restriction to Γ(N).

theorem TauCeti.EisensteinSeries.mem_congruenceEisensteinSubspace_iff {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : f ∈ congruenceEisensteinSubspace hΓ hk ↔ ModularForm.restrict ⋯ f ∈ primitiveEisensteinSubspace N hk

Membership in the Eisenstein subspace of M_k(Γ) is detected after restriction to the principal congruence subgroup.

theorem TauCeti.EisensteinSeries.isCompl_congruenceEisensteinSubspace_cuspFormSubmodule {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : IsCompl (congruenceEisensteinSubspace hΓ hk) (ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The cusp--Eisenstein decomposition on a subgroup Γ of SL(2, ℤ) containing Γ(N), in weight at least three. For Γ₁(N), take hΓ := CongruenceSubgroup.Gamma_le_Gamma1 N.

theorem TauCeti.EisensteinSeries.disjoint_congruenceEisensteinSubspace_cuspFormSubmodule {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : Disjoint (congruenceEisensteinSubspace hΓ hk) (ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The Eisenstein subspace of M_k(Γ) and the cusp-form submodule have zero intersection in weight at least three.

theorem TauCeti.EisensteinSeries.sup_congruenceEisensteinSubspace_cuspFormSubmodule_eq_top {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : congruenceEisensteinSubspace hΓ hk ⊔ ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k = ⊤

In weight at least three, the Eisenstein subspace of M_k(Γ) and the cusp forms together span all modular forms on Γ.