Eisenstein series with character

For Dirichlet characters ψ modulo u and φ modulo v and a weight k ≥ 3, the Eisenstein series of Diamond–Shurman §4.5, G_k^{ψ,φ}(z) = ∑_{c mod u} ∑_{d mod v} ∑_{e mod u} ψ(c) φ⁻¹(d) G_k^{(cv, d + ev)}(z), where G_k^{a} sums (m z + n)^(-k) over all (m, n) ≡ a mod uv. Collecting the terms, it is the series over all integer pairs x ∑_x w(x) (x₀ z + x₁)^(-k), w(x) = ψ(x₀ / v) φ⁻¹(x₁) if v ∣ x₀ and 0 otherwise, that is, ∑_{(c, d)} ψ(c) φ⁻¹(d) (c v z + d)^(-k).

We realize it as the residue-weighted Eisenstein series of TauCeti.NumberTheory.ModularForms.EisensteinSeries.Weighted, at any level N with u v ∣ N, and prove its transformation law (Diamond–Shurman §4.5): for γ ∈ Γ₀(N) with lower-right entry d, slashing by γ multiplies the series by ψ(d) φ(d). Hence the series is a modular form for Γ₁(N) lying in the nebentypus space M_k(N, ψφ).

No primitivity is assumed: the transformation law only uses that ψ and φ are characters. Primitivity matters for the q-expansion and the normalization of G_k^{ψ,φ} to E_k^{ψ,φ}, which are not treated in this file.

Main definitions

• TauCeti.EisensteinSeries.charWeight: the weight w as a function of residues modulo N.
• TauCeti.EisensteinSeries.charEisensteinSeriesMF: G_k^{ψ,φ} as a modular form of weight k for Γ₁(N).

Main results

• TauCeti.EisensteinSeries.charWeight_intCast: the weight evaluated at an integer pair.
• TauCeti.EisensteinSeries.charWeight_vecMul_inv: the transformation of the weight under Γ₀(N).
• TauCeti.EisensteinSeries.charEisensteinSeriesMF_apply: the series formula.
• TauCeti.EisensteinSeries.charEisensteinSeriesMF_mem_modFormCharSpace: G_k^{ψ,φ} lies in M_k(N, ψφ).
• TauCeti.EisensteinSeries.charEisensteinSeriesMF_eq_zero: it vanishes unless ψ(-1) φ(-1) = (-1)^k.

References

• F. Diamond and J. Shurman, A first course in modular forms, §4.5.
• T. Miyake, Modular forms, §7.1.

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

The weight defining the Eisenstein series with characters ψ modulo u and φ modulo v, as a function of a residue pair modulo N: for the least nonnegative representatives (m, n), it is ψ(m / v) φ⁻¹(n) when v ∣ m, and 0 otherwise. For u v ∣ N this does not depend on the choice of representatives (charWeight_intCast).

Equations

• TauCeti.EisensteinSeries.charWeight N ψ φ a = if v ∣ (a 0).val then ψ ↑((a 0).val / v) * φ⁻¹ ↑(a 1).val else 0

theorem TauCeti.EisensteinSeries.charWeight_intCast {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) [NeZero N] (huv : u * v ∣ N) (x : Fin 2 → ℤ) : charWeight N ψ φ (Int.cast ∘ x) = if ↑v ∣ x 0 then ψ ↑(x 0 / ↑v) * φ⁻¹ ↑(x 1) else 0

The weight at the reduction of an integer pair x: ψ(x₀ / v) φ⁻¹(x₁) if v ∣ x₀, and 0 otherwise.

theorem TauCeti.EisensteinSeries.charWeight_vecMul_inv {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) [NeZero N] (huv : u * v ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 N) (x : Fin 2 → ℤ) : charWeight N ψ φ (Int.cast ∘ Matrix.vecMul x ↑γ⁻¹) = ψ ↑(↑γ 1 1) * φ ↑(↑γ 1 1) * charWeight N ψ φ (Int.cast ∘ x)

The transformation of the weight under Γ₀(N). For γ ∈ Γ₀(N) with lower-right entry d, right multiplication by γ⁻¹ multiplies the weight by ψ(d) φ(d).

The Eisenstein series with character

theorem TauCeti.EisensteinSeries.weightedEisensteinSeries_charWeight_slash {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (huv : u * v ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 N) : SlashAction.map k γ (weightedEisensteinSeries (charWeight N ψ φ) k) = (ψ ↑(↑γ 1 1) * φ ↑(↑γ 1 1)) • weightedEisensteinSeries (charWeight N ψ φ) k

The transformation law (Diamond–Shurman, §4.5): for γ ∈ Γ₀(N) with lower-right entry d, the series weighted by charWeight N ψ φ satisfies G ∣[k] γ = ψ(d) φ(d) • G.

noncomputable def TauCeti.EisensteinSeries.charEisensteinSeriesMF {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (huv : u * v ∣ N) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

The Eisenstein series G_k^{ψ,φ} with characters ψ modulo u and φ modulo v, as a modular form of weight k ≥ 3 for Γ₁(N), where u v ∣ N: the series ∑_{x ∈ ℤ², v ∣ x₀} ψ(x₀ / v) φ⁻¹(x₁) (x₀ z + x₁)^(-k) (charEisensteinSeriesMF_apply), whose underlying function does not depend on N.

Equations

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

@[simp]

theorem TauCeti.EisensteinSeries.coe_charEisensteinSeriesMF {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (huv : u * v ∣ N) : ⇑(charEisensteinSeriesMF ψ φ hk huv) = weightedEisensteinSeries (charWeight N ψ φ) k

The Eisenstein series with character is the series weighted by charWeight N ψ φ.

theorem TauCeti.EisensteinSeries.charEisensteinSeriesMF_apply {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (huv : u * v ∣ N) (z : UpperHalfPlane) : (charEisensteinSeriesMF ψ φ hk huv) z = ∑' (x : Fin 2 → ℤ), (if ↑v ∣ x 0 then ψ ↑(x 0 / ↑v) * φ⁻¹ ↑(x 1) else 0) * EisensteinSeries.eisSummand k x z

The Eisenstein series with character, as a series over all integer pairs.

theorem TauCeti.EisensteinSeries.charEisensteinSeriesMF_mem_modFormCharSpace {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (huv : u * v ∣ N) : charEisensteinSeriesMF ψ φ hk huv ∈ modFormCharSpace k (MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) ψ * (DirichletCharacter.changeLevel ⋯) φ))

The nebentypus of the Eisenstein series with character: G_k^{ψ,φ} ∈ M_k(N, ψφ), the characters being raised to level N.

theorem TauCeti.EisensteinSeries.charEisensteinSeriesMF_eq_zero {u v N : ℕ} (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) {k : ℤ} [NeZero N] (hk : 3 ≤ k) (huv : u * v ∣ N) (h : ψ (-1) * φ (-1) ≠ (-1) ^ k) : charEisensteinSeriesMF ψ φ hk huv = 0

Parity: the Eisenstein series with character vanishes unless ψ(-1) φ(-1) = (-1)^k.