Character Eisenstein series in the primitive Eisenstein span

Residue-weighted lattice Eisenstein series are finite linear combinations of the primitive residue-class series. The coefficient of the primitive class a is the absolutely convergent sum ∑' r : ℕ, r⁻ᵏ W(r • a). Consequently every residue-weighted Eisenstein series belongs to the primitive Eisenstein subspace.

The same inclusion holds for every raised character Eisenstein series, including its normalized form. Restricting the raised lattice sum to Γ(N) gives a residue-weighted series by replacing the first lattice coordinate with its multiple by the raising parameter. Thus the existing prescribed-nebentypus Eisenstein subspace is contained in the congruence Eisenstein subspace, and its intersection with the image of the cusp forms of that nebentypus is zero.

The decomposition uses weightedEisensteinSeries_eq_tsum_eisensteinSeries, which separates integer pairs by their gcd and primitive residue class.

Main results

• weightedEisensteinSeriesMF_eq_sum_eisensteinSeriesMF: the finite primitive decomposition.
• restrict_charEisensteinSeriesMFRaise: restricted to Γ(N), a raised character Eisenstein series is the weighted series of raisedCharWeight.
• charEisensteinSeriesMFRaise_mem_congruenceEisensteinSubspace: the raised character inclusion.
• TauCeti.disjoint_eisensteinSubspace_range_cuspToModFormCharSpace: directness of the character Eisenstein span and the cusp-form image in weight at least three.

References

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

theorem TauCeti.EisensteinSeries.weightedEisensteinSeriesMF_eq_sum_eisensteinSeriesMF {N : ℕ} {k : ℤ} [NeZero N] (W : (Fin 2 → ZMod N) → ℂ) (hk : 3 ≤ k) : weightedEisensteinSeriesMF W hk = ∑ a : Fin 2 → ZMod N, (∑' (r : ℕ), (↑r ^ k)⁻¹ * W (r • a)) • ModularForm.eisensteinSeriesMF hk a

A residue-weighted Eisenstein series is a finite linear combination of the primitive residue-class series, with coefficients obtained by summing over positive gcds.

theorem TauCeti.EisensteinSeries.weightedEisensteinSeriesMF_mem_primitiveEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] (W : (Fin 2 → ZMod N) → ℂ) (hk : 3 ≤ k) : weightedEisensteinSeriesMF W hk ∈ primitiveEisensteinSubspace N hk

Every residue-weighted Eisenstein series belongs to the primitive Eisenstein span.

noncomputable def TauCeti.EisensteinSeries.raisedCharWeight {u v : ℕ} (N t : ℕ) (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (a : Fin 2 → ZMod N) : ℂ

The weight of the raised Eisenstein series with characters ψ modulo u and φ modulo v and raising parameter t, as a function of a residue pair modulo N: for the least nonnegative representatives (m, n), it is ψ(m / (t v)) φ⁻¹(n) when t v ∣ m, and 0 otherwise. Restricted to Γ(N), the raised series is the weighted Eisenstein series of this weight (restrict_charEisensteinSeriesMFRaise).

theorem TauCeti.EisensteinSeries.raisedCharWeight_def {u v : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (N t : ℕ) (a : Fin 2 → ZMod N) : raisedCharWeight N t ψ φ a = if t * v ∣ (a 0).val then ψ ↑((a 0).val / (t * v)) * φ⁻¹ ↑(a 1).val else 0

The defining expression for the weight of the raised character Eisenstein series.

theorem TauCeti.EisensteinSeries.restrict_charEisensteinSeriesMFRaise {N : ℕ} {k : ℤ} [NeZero N] {u v t : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) : ModularForm.restrict ⋯ (charEisensteinSeriesMFRaise ψ φ t hk htuv) = weightedEisensteinSeriesMF (raisedCharWeight N t ψ φ) hk

The raised character Eisenstein series as a weighted series. Restricted to Γ(N), the raised series G_k^{ψ,φ}(t z) is the Eisenstein series weighted by raisedCharWeight N t ψ φ: the substitution z ↦ t z multiplies the first coordinate of each lattice point by t.

theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_mem_congruenceEisensteinSubspace {N : ℕ} {k : ℤ} [NeZero N] {u v t : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) : charEisensteinSeriesMFRaise ψ φ t hk htuv ∈ congruenceEisensteinSubspace ⋯ hk

Every raised character Eisenstein series belongs to the congruence Eisenstein span at its target level, without requiring primitive characters or a parity assumption.

theorem TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise_mem_congruenceEisensteinSubspace {N : ℕ} [NeZero N] {u v t : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℕ} (hk : 3 ≤ ↑k) (htuv : t * (u * v) ∣ N) : normalizedCharEisensteinSeriesMFRaise ψ φ t hk htuv ∈ congruenceEisensteinSubspace ⋯ hk

Every normalized raised character Eisenstein series belongs to the congruence Eisenstein span at its target level.

theorem TauCeti.EisensteinSeries.CharIndex.form_mem_congruenceEisensteinSubspace {N : ℕ} [NeZero N] {k : ℕ} (a : CharIndex N k) (hk : 3 ≤ ↑k) : a.form hk ∈ congruenceEisensteinSubspace ⋯ hk

Every primitive, parity-compatible indexed character generator belongs to the congruence Eisenstein span.

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

The prescribed-nebentypus Eisenstein span is contained in the congruence Eisenstein span after forgetting character-space membership.

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

The prescribed-nebentypus Eisenstein subspace has zero intersection with the image of the cusp forms of the same nebentypus, in weight at least three.

theorem TauCeti.constantTermsOnEisensteinSubspace_injective {N k : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : Function.Injective fun (f : ↥(eisensteinSubspace χ hk)) => ModularForm.constantTerms ↑↑f

The constant terms at all cusps determine an element of the prescribed-nebentypus Eisenstein subspace. This is the injectivity half of identifying that subspace with the constant-term data; the converse spanning statement is separate.