feat: add definition of Eisenstein series (#9783)

This defines Eisenstein series of level N and shows that they are a slash invariant form. Also adds some pre-requisites for proving they are modular forms, which will be in the next PRs



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Mathlib.lean

@@ -2815,6 +2815,7 @@ import Mathlib.NumberTheory.MaricaSchoenheim
 import Mathlib.NumberTheory.Modular
 import Mathlib.NumberTheory.ModularForms.Basic
 import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -124,6 +124,13 @@ instance : Pow (SpecialLinearGroup n R) ℕ where
 instance : Inhabited (SpecialLinearGroup n R) :=
   ⟨1⟩
 
+/-- The transpose of a matrix in `SL(n, R)` -/
+def transpose (A : SpecialLinearGroup n R) : SpecialLinearGroup n R :=
+  ⟨A.1.transpose, A.1.det_transpose ▸ A.2⟩
+
+@[inherit_doc]
+scoped postfix:1024 "ᵀ" => SpecialLinearGroup.transpose
+
 section CoeLemmas
 
 variable (A B : SpecialLinearGroup n R)
@@ -158,6 +165,10 @@ theorem coe_pow (m : ℕ) : ↑ₘ(A ^ m) = ↑ₘA ^ m :=
   rfl
 #align matrix.special_linear_group.coe_pow Matrix.SpecialLinearGroup.coe_pow
 
+@[simp]
+lemma coe_transpose (A : SpecialLinearGroup n R) : ↑ₘAᵀ = (↑ₘA)ᵀ :=
+  rfl
+
 theorem det_ne_zero [Nontrivial R] (g : SpecialLinearGroup n R) : det ↑ₘg ≠ 0 := by
   rw [g.det_coe]
   norm_num
@@ -319,12 +330,70 @@ theorem fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type*} [Field R] (g
   simp_rw [eq_inv_of_mul_eq_one_right had, hg]
 #align matrix.special_linear_group.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero
 
+lemma isCoprime_row (A : SL(2, R)) (i : Fin 2): IsCoprime (A i 0) (A i 1) := by
+  refine match i with
+  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
+  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩ <;>
+  · simp_rw [det_coe A ▸ det_fin_two A.1]
+    ring
+
+lemma isCoprime_col (A : SL(2, R)) (j : Fin 2): IsCoprime (A 0 j) (A 1 j) := by
+    refine match j with
+    | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
+    | 1 => ⟨-(A 1 0), A 0 0, ?_⟩ <;>
+    · simp_rw [det_coe A ▸ det_fin_two A.1]
+      ring
+
 end SpecialCases
 
 end SpecialLinearGroup
 
 end Matrix
 
+namespace IsCoprime
+
+open Matrix MatrixGroups SpecialLinearGroup
+
+variable {R : Type*} [CommRing R]
+
+/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
+entries as its left or right column. -/
+lemma exists_SL2_col {a b : R} (hab : IsCoprime a b) (j : Fin 2):
+    ∃ g : SL(2, R), g 0 j = a ∧ g 1 j = b := by
+  obtain ⟨u, v, h⟩ := hab
+  refine match j with
+  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
+  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩ <;>
+  · rw [Matrix.det_fin_two_of, ← h]
+    ring
+
+/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
+entries as its top or bottom row. -/
+lemma exists_SL2_row {a b : R} (hab : IsCoprime a b) (i : Fin 2):
+    ∃ g : SL(2, R), g i 0 = a ∧ g i 1 = b := by
+  obtain ⟨u, v, h⟩ := hab
+  refine match i with
+  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
+  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩ <;>
+  · rw [Matrix.det_fin_two_of, ← h]
+    ring
+
+/-- A vector with coprime entries, right-multiplied by a matrix in `SL(2, R)`, has
+coprime entries. -/
+lemma vecMulSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
+    IsCoprime (vecMul v A.1 0) (vecMul v A.1 1) := by
+  obtain ⟨g, hg⟩ := hab.exists_SL2_row 0
+  have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }
+  simpa only [this] using isCoprime_row (g * A) 0
+
+/-- A vector with coprime entries, left-multiplied by a matrix in `SL(2, R)`, has
+coprime entries. -/
+lemma mulVecSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
+    IsCoprime (mulVec A.1 v 0) (mulVec A.1 v 1) := by
+  simpa only [← vecMul_transpose] using hab.vecMulSL A.transpose
+
+end IsCoprime
+
 namespace ModularGroup
 
 open MatrixGroups

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2024 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, David Loeffler
+-/
+import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
+import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+
+/-!
+# 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]
+-/
+
+noncomputable section
+
+open ModularForm UpperHalfPlane Complex Matrix
+
+open scoped MatrixGroups
+
+namespace EisensteinSeries
+
+variable (N : ℕ) (a : Fin 2 → ZMod N)
+
+section gammaSet_def
+
+/-- The set of pairs of coprime integers congruent to `a` mod `N`. -/
+def gammaSet := {v : Fin 2 → ℤ | (↑) ∘ v = a ∧ IsCoprime (v 0) (v 1)}
+
+lemma pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N) := by
+  refine fun u v huv ↦ ?_
+  contrapose! huv
+  obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv
+  exact hf.1.1.symm.trans hf.2.1
+
+/-- For level `N = 1`, the gamma sets are all equal. -/
+lemma gammaSet_one_eq (a a' : Fin 2 → ZMod 1) : gammaSet 1 a = gammaSet 1 a' :=
+  congr_arg _ (Subsingleton.elim _ _)
+
+/-- For level `N = 1`, the gamma sets are all equivalent; this is the equivalence. -/
+def gammaSet_one_equiv (a a' : Fin 2 → ZMod 1) : gammaSet 1 a ≃ gammaSet 1 a' :=
+  Equiv.Set.ofEq (gammaSet_one_eq a a')
+
+end gammaSet_def
+
+variable {N a}
+
+section gamma_action
+
+/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (vecMul a γ)`. -/
+lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ : SL(2, ℤ)) :
+    vecMul v γ ∈ gammaSet N (vecMul a γ) := by
+  refine ⟨?_, hv.2.vecMulSL γ⟩
+  have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
+  simp only [eq_intCast, Int.coe_castRingHom] at this
+  simp_rw [Function.comp, this, hv.1]
+  simp
+
+variable (a) in
+/-- The bijection between `GammaSets` given by multiplying by an element of `SL(2, ℤ)`. -/
+def gammaSetEquiv (γ : SL(2, ℤ)) : gammaSet N a ≃ gammaSet N (vecMul a γ) where
+  toFun v := ⟨vecMul v.1 γ, vecMul_SL2_mem_gammaSet v.2 γ⟩
+  invFun v := ⟨vecMul v.1 ↑(γ⁻¹), by
+      have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
+      rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this
+      simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
+        map_inv, mul_right_inv, SpecialLinearGroup.coe_one, vecMul_one]⟩
+  left_inv v := by simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, mul_inv_self,
+    SpecialLinearGroup.coe_one, vecMul_one]
+  right_inv v := by simp_rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul, inv_mul_self,
+    SpecialLinearGroup.coe_one, vecMul_one]
+
+end gamma_action
+
+section eisSummand
+
+/-- The function on `(Fin 2 → ℤ)` whose sum defines an Eisenstein series.-/
+def eisSummand (k : ℤ) (v : Fin 2 → ℤ) (z : ℍ) : ℂ := 1 / (v 0 * z.1 + v 1) ^ k
+
+/-- How the `eisSummand` function changes under the Moebius action. -/
+theorem eisSummand_SL2_apply (k : ℤ) (i : (Fin 2 → ℤ)) (A : SL(2, ℤ)) (z : ℍ) :
+    eisSummand k i (A • z) = (z.denom A) ^ k * eisSummand k (vecMul i A) z := by
+  simp only [eisSummand, specialLinearGroup_apply, algebraMap_int_eq, eq_intCast, ofReal_int_cast,
+    one_div, vecMul, vec2_dotProduct, Int.cast_add, Int.cast_mul]
+  have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : ((u * ((a * z + b) / (c * z + d)) + v) ^ k)⁻¹ =
+      (c * z + d) ^ k * (((u * a + v * c) * z + (u * b + v * d)) ^ k)⁻¹
+  · field_simp [hc]
+    ring_nf
+  apply h (hc := z.denom_ne_zero A)
+
+end eisSummand
+
+variable (a)
+
+/-- An Eisenstein series of weight `k` and level `Γ(N)`, with congruence condition `a`. -/
+def eisensteinSeries (k : ℤ) (z : ℍ) : ℂ := ∑' x : gammaSet N a, eisSummand k x z
+
+lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
+    eisensteinSeries a k ∣[k] γ = eisensteinSeries (vecMul a γ) k := by
+  ext1 z
+  simp_rw [SL_slash, slash_def, slash, det_coe', ofReal_one, one_zpow, mul_one, zpow_neg,
+    mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| z.denom_ne_zero _), mul_comm,
+    eisensteinSeries, ← UpperHalfPlane.sl_moeb, eisSummand_SL2_apply, tsum_mul_left]
+  erw [(gammaSetEquiv a γ).tsum_eq (eisSummand k · z)]
+
+/-- The SlashInvariantForm defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
+  and congruence condition given by `a : Fin 2 → ZMod N`. -/
+def eisensteinSeries_SIF (k : ℤ) : SlashInvariantForm (Gamma N) k where
+  toFun := eisensteinSeries a k
+  slash_action_eq' A := by rw [subgroup_slash, ← SL_slash, eisensteinSeries_slash_apply,
+      (Gamma_mem' N A).mp A.2, SpecialLinearGroup.coe_one, vecMul_one]