Eisenstein Series

Main definitions

• We define Eisenstein series of level Γ(N) for any N : ℕ and weight k : ℤ as the infinite sum ∑' v : (Fin 2 → ℤ), (1 / (v 0 * z + v 1) ^ k), where z : ℍ and v ranges over all pairs of coprime integers congruent to a fixed pair (a, b) modulo N. Note that by using (Fin 2 → ℤ) instead of ℤ × ℤ we can state all of the required equivalences using matrices and vectors, which makes working with them more convenient.

• We show that they define a slash invariant form of level Γ(N) and weight k.

References

• [F. Diamond and J. Shurman, A First Course in Modular Forms][diamondshurman2005]

def EisensteinSeries.gammaSet (N : ℕ) (a : Fin 2 → ZMod N) : Set (Fin 2 → ℤ)

The set of pairs of coprime integers congruent to a mod N.

theorem EisensteinSeries.pairwise_disjoint_gammaSet (N : ℕ) : Pairwise (Function.onFun Disjoint (gammaSet N))

theorem EisensteinSeries.gammaSet_one_eq (a a' : Fin 2 → ZMod 1) : gammaSet 1 a = gammaSet 1 a'

For level N = 1, the gamma sets are all equal.

def EisensteinSeries.gammaSet_one_equiv (a a' : Fin 2 → ZMod 1) : ↑(gammaSet 1 a) ≃ ↑(gammaSet 1 a')

For level N = 1, the gamma sets are all equivalent; this is the equivalence.

theorem EisensteinSeries.vecMul_SL2_mem_gammaSet {N : ℕ} {a : Fin 2 → ZMod N} {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Matrix.vecMul v ↑γ ∈ gammaSet N (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

Right-multiplying by γ ∈ SL(2, ℤ) sends gammaSet N a to gammaSet N (a ᵥ* γ).

def EisensteinSeries.gammaSetEquiv {N : ℕ} (a : Fin 2 → ZMod N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(gammaSet N a) ≃ ↑(gammaSet N (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))

The bijection between GammaSets given by multiplying by an element of SL(2, ℤ).

def EisensteinSeries.eisSummand (k : ℤ) (v : Fin 2 → ℤ) (z : UpperHalfPlane) : ℂ

The function on (Fin 2 → ℤ) whose sum defines an Eisenstein series.

theorem EisensteinSeries.eisSummand_SL2_apply (k : ℤ) (i : Fin 2 → ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : eisSummand k i (A • z) = UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z ^ k * eisSummand k (Matrix.vecMul i ↑A) z

How the eisSummand function changes under the Moebius action.

def eisensteinSeries {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (z : UpperHalfPlane) : ℂ

An Eisenstein series of weight k and level Γ(N), with congruence condition a.

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

def EisensteinSeries.eisensteinSeries_SIF {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) : SlashInvariantForm (CongruenceSubgroup.Gamma N) k

The SlashInvariantForm defined by an Eisenstein series of weight k : ℤ, level Γ(N), and congruence condition given by a : Fin 2 → ZMod N.

theorem EisensteinSeries.eisensteinSeries_SIF_apply {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (z : UpperHalfPlane) : (eisensteinSeries_SIF a k) z = eisensteinSeries a k z