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.

Equations

• EisensteinSeries.gammaSet N a = {v : Fin 2 → ℤ | Int.cast ∘ v = a ∧ IsCoprime (v 0) (v 1)}

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

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

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

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

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

Equations

• EisensteinSeries.gammaSet_one_equiv a a' = Equiv.Set.ofEq ⋯

theorem EisensteinSeries.vecMul_SL2_mem_gammaSet {N : ℕ} {a : Fin 2 → ZMod N} {v : Fin 2 → ℤ} (hv : v ∈ EisensteinSeries.gammaSet N a) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Matrix.vecMul v ↑γ ∈ EisensteinSeries.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) ℤ) : ↑(EisensteinSeries.gammaSet N a) ≃ ↑(EisensteinSeries.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, ℤ).

Equations

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

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

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

Equations

• EisensteinSeries.eisSummand k v z = 1 / (↑(v 0) * ↑z + ↑(v 1)) ^ k

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

How the eisSummand function changes under the Moebius action.

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

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

Equations

• EisensteinSeries.eisensteinSeries a k z = ∑' (x : ↑(EisensteinSeries.gammaSet N a)), EisensteinSeries.eisSummand k (↑x) z

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

def EisensteinSeries.eisensteinSeries_SIF {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) : SlashInvariantForm (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.

Equations

• EisensteinSeries.eisensteinSeries_SIF a k = { toFun := EisensteinSeries.eisensteinSeries a k, slash_action_eq' := ⋯ }