The Eisenstein projection and nebentypus

In weight at least three, the congruence Eisenstein subspace is complementary to the cusp forms. Projection along this complement preserves every cusp constant term and is uniquely determined by that property among Eisenstein forms.

For Γ₁(N), the projection commutes with diamond operators: slashing permutes the primitive residue-class Eisenstein series, while diamond operators preserve cusp forms. Consequently the Eisenstein and cusp components of a form with prescribed nebentypus have that same nebentypus. This gives a complementary decomposition inside M_k(N, χ) using the restriction of the congruence Eisenstein subspace. Identifying this subspace with the span of the prescribed primitive-character Eisenstein series is a separate spanning statement.

Main results

• congruenceEisensteinProjection: projection to the congruence Eisenstein subspace, with range, kernel and idempotence characterizations.
• constantTerms_congruenceEisensteinProjection: projection preserves all cusp constant terms.
• congruenceEisensteinProjection_eq_iff_constantTerms_eq: its constant-term characterization.
• congruenceEisensteinProjection_diamondOp: pointwise equivariance under diamond operators.
• isCompl_congruenceEisensteinSubspace_charSpace_range_cuspToModFormCharSpace: the complementary decomposition with fixed nebentypus.

References

• F. Diamond and J. Shurman, A first course in modular forms, Sections 4.2 and 4.5.

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

The projection to the congruence Eisenstein subspace along the cusp forms.

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

The Eisenstein projection is the projection associated to the complementary subspaces.

@[simp]

theorem TauCeti.EisensteinSeries.range_congruenceEisensteinProjection {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : LinearMap.range (congruenceEisensteinProjection hΓ hk) = congruenceEisensteinSubspace hΓ hk

The range of the Eisenstein projection is the congruence Eisenstein subspace.

@[simp]

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

The kernel of the Eisenstein projection is the cusp-form submodule.

theorem TauCeti.EisensteinSeries.isIdempotentElem_congruenceEisensteinProjection {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) : IsIdempotentElem (congruenceEisensteinProjection hΓ hk)

The Eisenstein projection is an idempotent endomorphism.

@[simp]

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

The Eisenstein component belongs to the congruence Eisenstein subspace.

theorem TauCeti.EisensteinSeries.sub_congruenceEisensteinProjection_mem_cuspFormSubmodule {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 - (congruenceEisensteinProjection hΓ hk) f ∈ ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

The difference between a form and its Eisenstein component is cuspidal.

@[simp]

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_eq_self_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) : (congruenceEisensteinProjection hΓ hk) f = f ↔ f ∈ congruenceEisensteinSubspace hΓ hk

A form is fixed by the Eisenstein projection exactly when it is Eisenstein.

@[simp]

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_eq_zero_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) : (congruenceEisensteinProjection hΓ hk) f = 0 ↔ f ∈ ModularForm.cuspFormSubmodule (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k

The Eisenstein component vanishes exactly when the original form is cuspidal.

@[simp]

theorem TauCeti.EisensteinSeries.constantTermAt_congruenceEisensteinProjection {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic] (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (ModularForm.constantTermAt γ) ((congruenceEisensteinProjection hΓ hk) f) = (ModularForm.constantTermAt γ) f

The Eisenstein component has the same constant term at every cusp as the original form.

@[simp]

theorem TauCeti.EisensteinSeries.constantTerms_congruenceEisensteinProjection {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic] (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : ModularForm.constantTerms ((congruenceEisensteinProjection hΓ hk) f) = ModularForm.constantTerms f

The Eisenstein projection preserves the collection of all cusp constant terms.

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_eq_iff_constantTerms_eq {N : ℕ} {k : ℤ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic] (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (hk : 3 ≤ k) (f e : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (he : e ∈ congruenceEisensteinSubspace hΓ hk) : (congruenceEisensteinProjection hΓ hk) f = e ↔ ModularForm.constantTerms e = ModularForm.constantTerms f

Among Eisenstein forms, the projection of f is characterized by having all the same cusp constant terms as f.

theorem TauCeti.EisensteinSeries.diamondOp_mem_congruenceEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (d : (ZMod N)ˣ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ congruenceEisensteinSubspace ⋯ hk) : (diamondOp k d) f ∈ congruenceEisensteinSubspace ⋯ hk

Diamond operators preserve the congruence Eisenstein subspace of Γ₁(N).

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_commute_diamondOp {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (d : (ZMod N)ˣ) : Commute (congruenceEisensteinProjection ⋯ hk) (diamondOp k d)

The Eisenstein projection on Γ₁(N) commutes with every diamond operator.

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_diamondOp {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (d : (ZMod N)ˣ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (congruenceEisensteinProjection ⋯ hk) ((diamondOp k d) f) = (diamondOp k d) ((congruenceEisensteinProjection ⋯ hk) f)

Projecting the diamond translate of a form agrees with translating its Eisenstein component.

theorem TauCeti.EisensteinSeries.congruenceEisensteinProjection_mem_modFormCharSpace {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (χ : (ZMod N)ˣ →* ℂˣ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) : (congruenceEisensteinProjection ⋯ hk) f ∈ modFormCharSpace k χ

The Eisenstein component preserves the prescribed nebentypus of a modular form.

theorem TauCeti.EisensteinSeries.isCompl_congruenceEisensteinSubspace_charSpace_range_cuspToModFormCharSpace {N : ℕ} {k : ℤ} [NeZero N] (hk : 3 ≤ k) (χ : (ZMod N)ˣ →* ℂˣ) : IsCompl (Submodule.comap (modFormCharSpace k χ).subtype (congruenceEisensteinSubspace ⋯ hk)) (cuspToModFormCharSpace k χ).range

In weight at least three, the restriction of the congruence Eisenstein subspace to a nebentypus space is complementary to the cusp forms of that same nebentypus.