The Eisenstein series with character span the Eisenstein space

In weight k ≥ 3, the normalized raised Eisenstein series E_k^(ψ, φ, t), indexed by TauCeti.EisensteinSeries.CharIndex N k, span the Eisenstein subspace TauCeti.EisensteinSeries.congruenceEisensteinSubspace of M_k(Γ₁(N)), the complement of the cusp forms (Diamond–Shurman, Theorem 4.5.2). Together with their linear independence they form a basis of it. At a level N ∉ {1, 2, 4} there are as many of them as there are cusps, so that

dim M_k(Γ₁(N)) = dim S_k(Γ₁(N)) + ε∞(Γ₁(N)),

where ε∞(Γ₁(N)) is the number of cusps of Γ₁(N). Restricted to a nebentypus χ, the series of nebentypus χ span the Eisenstein part of M_k(N, χ): the span TauCeti.eisensteinSubspace χ is exactly the intersection of M_k(N, χ) with the Eisenstein subspace, and so is complementary to the image of S_k(N, χ).

The proof compares dimensions. The series lie in the Eisenstein subspace and are linearly independent. Conversely the Eisenstein subspace meets the cusp forms trivially, so the constant terms embed it into the functions on the cusps (TauCeti.ModularForm.finrank_le_card_cuspOrbit_of_disjoint), and at N ∉ {1, 2, 4} the series are as many as the cusps (TauCeti.EisensteinSeries.CharIndex.card_eq_card_cuspOrbit_Gamma1). At the levels 1, 2 and 4 the constant terms are read at explicit cusp representatives instead (TauCeti.ModularForm.finrank_le_natCard_of_disjoint). In odd weight every form vanishes when N ∣ 2, since then -1 ∈ Γ₁(N), and the irregular cusp 1/2 of Γ₁(4) carries no constant term. The remaining representatives are as many as the series (TauCeti.EisensteinSeries.CharIndex.card_one, card_two, card_four). For a fixed nebentypus, a form of nebentypus χ in the span of all the series lies in the span of those of nebentypus χ, because the character spaces M_k(N, ψ) are independent.

Main results

• TauCeti.EisensteinSeries.span_range_form_eq_congruenceEisensteinSubspace: the series span the Eisenstein subspace of M_k(Γ₁(N)).
• TauCeti.EisensteinSeries.finrank_congruenceEisensteinSubspace: its dimension is the number of series.
• TauCeti.EisensteinSeries.finrank_congruenceEisensteinSubspace_Gamma1: at N ∉ {1, 2, 4}, its dimension is the number of cusps of Γ₁(N).
• TauCeti.finrank_modularForm_Gamma1_eq_finrank_cuspForm_add_card_cuspOrbit: dim M_k(Γ₁(N)) = dim S_k(Γ₁(N)) + ε∞(Γ₁(N)) at N ∉ {1, 2, 4}.
• TauCeti.eisensteinSubspace_eq_comap_congruenceEisensteinSubspace: the series of nebentypus χ span the Eisenstein part of M_k(N, χ).
• TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpace: the cusp–Eisenstein decomposition M_k(N, χ) = S_k(N, χ) ⊕ E_k(N, χ) with E_k(N, χ) spanned by the series.

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 4.5, Theorem 4.5.2, and Section 3.8 for the cusps of Γ₁(N).

theorem TauCeti.EisensteinSeries.span_range_form_eq_congruenceEisensteinSubspace {N k : ℕ} [NeZero N] (hk : 3 ≤ ↑k) : Submodule.span ℂ (Set.range fun (a : CharIndex N k) => a.form hk) = congruenceEisensteinSubspace ⋯ hk

The Eisenstein series with character span the Eisenstein space (Diamond–Shurman, Theorem 4.5.2): in weight k ≥ 3, the normalized raised series E_k^(ψ, φ, t) span the Eisenstein subspace of M_k(Γ₁(N)), the complement of the cusp forms.

theorem TauCeti.EisensteinSeries.finrank_congruenceEisensteinSubspace {N k : ℕ} [NeZero N] (hk : 3 ≤ ↑k) : Module.finrank ℂ ↥(congruenceEisensteinSubspace ⋯ hk) = Nat.card (CharIndex N k)

In weight k ≥ 3, the Eisenstein subspace of M_k(Γ₁(N)) has dimension the number of Eisenstein indices.

theorem TauCeti.EisensteinSeries.finrank_congruenceEisensteinSubspace_Gamma1 {N k : ℕ} [NeZero N] (hN : 2 < N) (hN4 : N ≠ 4) (hk : 3 ≤ ↑k) : Module.finrank ℂ ↥(congruenceEisensteinSubspace ⋯ hk) = Nat.card (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma1 N)).CuspOrbit

In weight k ≥ 3 and at a level N ∉ {1, 2, 4}, the Eisenstein subspace of M_k(Γ₁(N)) has dimension the number of cusps of Γ₁(N).

theorem TauCeti.finrank_modularForm_Gamma1_eq_finrank_cuspForm_add_card_cuspOrbit {N k : ℕ} [NeZero N] (hN : 2 < N) (hN4 : N ≠ 4) (hk : 3 ≤ ↑k) : Module.finrank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) ↑k) = Module.finrank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) ↑k) + Nat.card (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma1 N)).CuspOrbit

The Eisenstein part of the dimension of M_k(Γ₁(N)): in weight k ≥ 3 and at a level N ∉ {1, 2, 4}, the modular forms on Γ₁(N) have dimension ε∞(Γ₁(N)) more than the cusp forms, where ε∞(Γ₁(N)) is the number of cusps of Γ₁(N).

theorem TauCeti.eisensteinSubspace_eq_comap_congruenceEisensteinSubspace {N k : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : eisensteinSubspace χ hk = Submodule.comap (modFormCharSpace (↑k) χ).subtype (EisensteinSeries.congruenceEisensteinSubspace ⋯ hk)

The Eisenstein series of nebentypus χ span the Eisenstein part of M_k(N, χ): in weight k ≥ 3, a form of nebentypus χ lies in the Eisenstein subspace of M_k(Γ₁(N)) exactly when it is a linear combination of the series E_k^(ψ, φ, t) whose induced nebentypus is χ.

theorem TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpace {N k : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : IsCompl (eisensteinSubspace χ hk) (cuspToModFormCharSpace (↑k) χ).range

The cusp–Eisenstein decomposition of M_k(N, χ): in weight k ≥ 3, the span of the Eisenstein series of nebentypus χ is a complement of the image of S_k(N, χ) in M_k(N, χ).