feat(NumberTheory/ModularForms/EisensteinSeries): Update gammaSet (#27840)

We  redefine gammaSet to include vectors with non-trivial gcd.  This is useful for giving the q-expansions of Eisenstein series at level one. Which can be seen here #27606  (these equivalences are used in `tsum_prod_eisSummand_eq_riemannZeta_eisensteinSeries` in the QExpansions file).

Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Author: CBirkbeck

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

@@ -3,8 +3,9 @@ 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.Algebra.EuclideanDomain.Int
 import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
-import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
+import Mathlib.RingTheory.EuclideanDomain
 
 /-!
 # Eisenstein Series
@@ -25,52 +26,139 @@ import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
 
 noncomputable section
 
-open ModularForm UpperHalfPlane Complex Matrix CongruenceSubgroup
+open ModularForm UpperHalfPlane Complex Matrix CongruenceSubgroup Set
 
 open scoped MatrixGroups
 
 namespace EisensteinSeries
 
-variable (N : ℕ) (a : Fin 2 → ZMod N)
+variable (N r : ℕ) (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)}
+/-- The set of pairs of integers congruent to `a` mod `N` and with `gcd` equal to `r`. -/
+def gammaSet := {v : Fin 2 → ℤ | (↑) ∘ v = a ∧ (v 0).gcd (v 1) = r}
 
 open scoped Function in -- required for scoped `on` notation
-lemma pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N) := by
+lemma pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N r) := 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' :=
+lemma gammaSet_one_const (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a = gammaSet 1 r a' :=
   congr_arg _ (Subsingleton.elim _ _)
 
+/-- For level `N = 1`, the gamma sets simplify to only a `gcd` condition. -/
+lemma gammaSet_one_eq (a : Fin 2 → ZMod 1) :
+    gammaSet 1 r a = {v : Fin 2 → ℤ | (v 0).gcd (v 1) = r} := by
+  simp [gammaSet, Subsingleton.eq_zero]
+
+lemma gammaSet_one_mem_iff (v : Fin 2 → ℤ) : v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r := by
+  simp [gammaSet, Subsingleton.eq_zero]
+
 /-- 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.setCongr (gammaSet_one_eq a a')
+def gammaSet_one_equiv (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a ≃ gammaSet 1 r a' :=
+  Equiv.setCongr (gammaSet_one_const r a a')
+
+/-- The map from `Fin 2 → ℤ` sending `![a,b]` to `a.gcd b`. -/
+abbrev finGcdMap (v : Fin 2 → ℤ) : ℕ := (v 0).gcd (v 1)
+
+lemma finGcdMap_div {r : ℕ} [NeZero r] (v : Fin 2 → ℤ) (hv : finGcdMap v = r) :
+    IsCoprime ((v / r) 0 ) ((v / r) 1) := by
+  rw [← hv]
+  apply isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
+  have := NeZero.ne r
+  aesop
+
+lemma finGcdMap_smul {r : ℕ} (a : ℤ) {v : Fin 2 → ℤ} (hv : finGcdMap v = r) :
+    finGcdMap (a • v) = a.natAbs * r := by
+  simp [finGcdMap, Int.gcd_mul_left, hv]
+
+/-- An abbreviation of the map which divides a integer vector by an integer. -/
+abbrev divIntMap (r : ℤ) {m : ℕ} (v : Fin m → ℤ) : Fin m → ℤ := v / r
+
+lemma mem_gammaSet_one (v : Fin 2 → ℤ) : v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1) := by
+  rw [gammaSet_one_mem_iff, Int.isCoprime_iff_gcd_eq_one]
+
+lemma gammaSet_div_gcd {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ (gammaSet 1 r 0)) (i : Fin 2) :
+   (r : ℤ) ∣ v i := by
+  fin_cases i <;> simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]
+
+lemma gammaSet_div_gcd_to_gammaSet10_bijection (r : ℕ) [NeZero r] :
+    Set.BijOn (divIntMap r) (gammaSet 1 r 0) (gammaSet 1 1 0) := by
+  refine ⟨?_, ?_, ?_⟩
+  · intro x hx
+    simp only [divIntMap, mem_gammaSet_one] at *
+    exact finGcdMap_div _ hx.2
+  · intro x hx v hv hv2
+    ext i
+    exact (Int.ediv_left_inj (gammaSet_div_gcd hx i) (gammaSet_div_gcd hv i)).mp
+      (congr_fun hv2 i)
+  · intro x hx
+    use r • x
+    simp only [nsmul_eq_mul, divIntMap, Int.cast_natCast]
+    constructor
+    · rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
+      exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩
+    · ext i
+      simp_all [NeZero.ne r]
+
+lemma gammaSet_eq_gcd_mul_divIntMap {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ gammaSet 1 r 0) :
+    v = r • (divIntMap r v) := by
+  by_cases hr : r = 0
+  · have hv := hv.2
+    simp only [hr, Fin.isValue, Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_smul] at *
+    ext i
+    fin_cases i <;> simp [hv]
+  · ext i
+    simp_all [Pi.smul_apply, divIntMap, ← Int.mul_ediv_assoc _ (gammaSet_div_gcd hv i)]
+
+/-- The equivalence between `gammaSet 1 r 0` and `gammaSet 1 1 0` for non-zero `r`. -/
+def gammaSetDivGcdEquiv (r : ℕ) [NeZero r] : gammaSet 1 r 0 ≃ gammaSet 1 1 0 :=
+    Set.BijOn.equiv _ (gammaSet_div_gcd_to_gammaSet10_bijection r)
+
+/-- The equivalence between `(Fin 2 → ℤ)` and `Σ n : ℕ, gammaSet 1 n 0)` . -/
+def gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (Σ r : ℕ, gammaSet 1 r 0) := by
+  apply (Equiv.sigmaFiberEquiv finGcdMap).symm.trans
+  refine Equiv.sigmaCongrRight fun b => ?_
+  apply Equiv.setCongr
+  rw [gammaSet_one_eq]
+  rfl
+
+@[simp]
+lemma gammaSetDivGcdSigmaEquiv_symm_eq (v : Σ r : ℕ, gammaSet 1 r 0) :
+    (gammaSetDivGcdSigmaEquiv.symm v) = v.2 := rfl
 
 end gammaSet_def
 
-variable {N a}
+variable {N a r} [NeZero r]
 
 section gamma_action
 
+/-- Right-multiplying a vector by a matrix in `SL(2, ℤ)` doesn't change its gcd. -/
+lemma vecMulSL_gcd {v : Fin 2 → ℤ} (hab : finGcdMap v = r) (A : SL(2, ℤ)) :
+    finGcdMap (v ᵥ* A.1) = r := by
+  have hvr : v = r • (v / r) := by
+    ext i
+    refine Eq.symm (Int.mul_ediv_cancel' ?_)
+    fin_cases i <;> simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]
+  rw [hvr, smul_vecMul]
+  simpa using finGcdMap_smul r (Int.isCoprime_iff_gcd_eq_one.mp ((finGcdMap_div v hab).vecMulSL A))
+
 /-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (a ᵥ* γ)`. -/
-lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ : SL(2, ℤ)) :
-    v ᵥ* γ ∈ gammaSet N (a ᵥ* γ) := by
-  refine ⟨?_, hv.2.vecMulSL γ⟩
+lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N r a)
+    (γ : SL(2, ℤ)) : v ᵥ* γ ∈ gammaSet N r (a ᵥ* γ) := by
+  refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
   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_def, 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 (a ᵥ* γ) where
+def gammaSetEquiv (γ : SL(2, ℤ)) : gammaSet N r a ≃ gammaSet N r (a ᵥ* γ) where
   toFun v := ⟨v.1 ᵥ* γ, vecMul_SL2_mem_gammaSet v.2 γ⟩
   invFun v := ⟨v.1 ᵥ* ↑(γ⁻¹), by
       have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
@@ -106,7 +194,7 @@ end eisSummand
 variable (a)
 
 /-- An Eisenstein series of weight `k` and level `Γ(N)`, with congruence condition `a`. -/
-def _root_.eisensteinSeries (k : ℤ) (z : ℍ) : ℂ := ∑' x : gammaSet N a, eisSummand k x z
+def _root_.eisensteinSeries (k : ℤ) (z : ℍ) : ℂ := ∑' x : gammaSet N 1 a, eisSummand k x z
 
 lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
     eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* γ) k := by

Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

@@ -38,11 +38,11 @@ namespace EisensteinSeries
 /-- The sum defining the Eisenstein series (of weight `k` and level `Γ(N)` with congruence
 condition `a : Fin 2 → ZMod N`) converges locally uniformly on `ℍ`. -/
 theorem eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : ℕ} (a : Fin 2 → ZMod N) :
-    TendstoLocallyUniformly (fun (s : Finset (gammaSet N a)) ↦ (∑ x ∈ s, eisSummand k x ·))
+    TendstoLocallyUniformly (fun (s : Finset (gammaSet N 1 a)) ↦ (∑ x ∈ s, eisSummand k x ·))
       (eisensteinSeries a k ·) Filter.atTop := by
   have hk' : (2 : ℝ) < k := by norm_cast
-  have p_sum : Summable fun x : gammaSet N a ↦ ‖x.val‖ ^ (-k) :=
-    mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N a)
+  have p_sum : Summable fun x : gammaSet N 1 a ↦ ‖x.val‖ ^ (-k) :=
+    mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N 1 a)
   simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]
   intro K hK
   obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact hK
@@ -54,7 +54,7 @@ theorem eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : 
 /-- Variant of `eisensteinSeries_tendstoLocallyUniformly` formulated with maps `ℂ → ℂ`, which is
 nice to have for holomorphicity later. -/
 lemma eisensteinSeries_tendstoLocallyUniformlyOn {k : ℤ} {N : ℕ} (hk : 3 ≤ k)
-    (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N a)) ↦
+    (a : Fin 2 → ZMod N) : TendstoLocallyUniformlyOn (fun (s : Finset (gammaSet N 1 a)) ↦
       ↑ₕ(fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k x z)) (↑ₕ(eisensteinSeries_SIF a k).toFun)
           Filter.atTop {z : ℂ | 0 < z.im} := by
   rw [← Subtype.coe_image_univ {z : ℂ | 0 < z.im}]

Mathlib/RingTheory/EuclideanDomain.lean

@@ -51,6 +51,15 @@ theorem isCoprime_div_gcd_div_gcd (hq : q ≠ 0) :
         (EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_right _ _).symm <|
       gcd_ne_zero_of_right hq
 
+/-- This is a version of `isCoprime_div_gcd_div_gcd` which replaces the `q ≠ 0` assumption with
+`gcd p q ≠ 0`. -/
+theorem isCoprime_div_gcd_div_gcd_of_gcd_ne_zero (hpq : GCDMonoid.gcd p q ≠ 0) :
+    IsCoprime (p / GCDMonoid.gcd p q) (q / GCDMonoid.gcd p q) :=
+  (gcd_isUnit_iff _ _).1 <|
+    isUnit_gcd_of_eq_mul_gcd
+        (EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_left _ _).symm
+        (EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_right _ _).symm <| hpq
+
 end GCDMonoid
 
 namespace EuclideanDomain