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 r : ℕ) (a : Fin 2 → ZMod N) : Set (Fin 2 → ℤ)

The set of pairs of integers congruent to a mod N and with gcd equal to r.

Equations

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

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

theorem EisensteinSeries.gammaSet_one_const (r : ℕ) (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a = gammaSet 1 r a'

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

theorem EisensteinSeries.gammaSet_one_eq (r : ℕ) (a : Fin 2 → ZMod 1) : gammaSet 1 r a = {v : Fin 2 → ℤ | (v 0).gcd (v 1) = r}

For level N = 1, the gamma sets simplify to only a gcd condition.

theorem EisensteinSeries.gammaSet_one_mem_iff (r : ℕ) (v : Fin 2 → ℤ) : v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r

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

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

Equations

• EisensteinSeries.gammaSet_one_equiv r a a' = Equiv.setCongr ⋯

@[reducible, inline]

abbrev EisensteinSeries.finGcdMap (v : Fin 2 → ℤ) : ℕ

The map from Fin 2 → ℤ sending ![a,b] to a.gcd b.

Equations

• EisensteinSeries.finGcdMap v = (v 0).gcd (v 1)

theorem EisensteinSeries.finGcdMap_div {r : ℕ} [NeZero r] (v : Fin 2 → ℤ) (hv : finGcdMap v = r) : IsCoprime ((v / ↑r) 0) ((v / ↑r) 1)

theorem EisensteinSeries.finGcdMap_smul {r : ℕ} (a : ℤ) {v : Fin 2 → ℤ} (hv : finGcdMap v = r) : finGcdMap (a • v) = a.natAbs * r

@[reducible, inline]

abbrev EisensteinSeries.divIntMap (r : ℤ) {m : ℕ} (v : Fin m → ℤ) : Fin m → ℤ

An abbreviation of the map which divides an integer vector by an integer.

Equations

• EisensteinSeries.divIntMap r v = v / ↑r

theorem EisensteinSeries.mem_gammaSet_one (v : Fin 2 → ℤ) : v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

theorem EisensteinSeries.gammaSet_div_gcd {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ gammaSet 1 r 0) (i : Fin 2) : ↑r ∣ v i

theorem EisensteinSeries.gammaSet_div_gcd_to_gammaSet10_bijection (r : ℕ) [NeZero r] : Set.BijOn (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)

theorem EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ gammaSet 1 r 0) : v = r • divIntMap (↑r) v

noncomputable def EisensteinSeries.gammaSetDivGcdEquiv (r : ℕ) [NeZero r] : ↑(gammaSet 1 r 0) ≃ ↑(gammaSet 1 1 0)

The equivalence between gammaSet 1 r 0 and gammaSet 1 1 0 for non-zero r.

Equations

• EisensteinSeries.gammaSetDivGcdEquiv r = Set.BijOn.equiv (EisensteinSeries.divIntMap ↑r) ⋯

@[simp]

theorem EisensteinSeries.gammaSetDivGcdEquiv_eq (r : ℕ) [NeZero r] (v : ↑(gammaSet 1 r 0)) : ↑((gammaSetDivGcdEquiv r) v) = divIntMap ↑r ↑v

def EisensteinSeries.gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (r : ℕ) × ↑(gammaSet 1 r 0)

The equivalence between (Fin 2 → ℤ) and Σ n : ℕ, gammaSet 1 n 0) .

Equations

• EisensteinSeries.gammaSetDivGcdSigmaEquiv = (Equiv.sigmaFiberEquiv EisensteinSeries.finGcdMap).symm.trans (Equiv.sigmaCongrRight fun (b : ℕ) => Equiv.subtypeEquivProp ⋯)

@[simp]

theorem EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq (v : (r : ℕ) × ↑(gammaSet 1 r 0)) : gammaSetDivGcdSigmaEquiv.symm v = ↑v.snd

theorem EisensteinSeries.vecMulSL_gcd {r : ℕ} [NeZero r] {v : Fin 2 → ℤ} (hab : finGcdMap v = r) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : finGcdMap (Matrix.vecMul v ↑A) = r

Right-multiplying a vector by a matrix in SL(2, ℤ) doesn't change its gcd.

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

noncomputable 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 = (↑(v 0) * ↑z + ↑(v 1)) ^ (-k)

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.

noncomputable def 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 a k z = ∑' (x : ↑(EisensteinSeries.gammaSet N 1 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 a k) = eisensteinSeries (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k

noncomputable def EisensteinSeries.eisensteinSeriesSIF {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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.

Equations

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

@[deprecated EisensteinSeries.eisensteinSeriesSIF (since := "2026-02-10")]

def EisensteinSeries.eisensteinSeries_SIF {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N)) k

Alias of EisensteinSeries.eisensteinSeriesSIF.

---

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 = @EisensteinSeries.eisensteinSeriesSIF

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

@[deprecated EisensteinSeries.eisensteinSeriesSIF_apply (since := "2026-02-10")]

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

Alias of EisensteinSeries.eisensteinSeriesSIF_apply.