refactor : add namespace UpperHalfPlane.ModularGroup (#7885)

Rename some definitions and theorems about $SL(2, ℤ)$ in `Analysis/Complex/UpperHalfPlane/Basic.lean` to place them in the namespace `UpperHalfPlane.ModularGroup`, in order to avoid the confusion with definitions and theorems about $SL(2, ℝ)$. For example, `UpperHalfPlane.det_coe'` is renamed to `UpperHalfPlane.ModularGroup.det_coe'`, because we will have `UpperHalfPlane.SL2R.det_coe'`.



Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -282,12 +282,15 @@ instance : MulAction GL(2, ℝ)⁺ ℍ where
 
 section ModularScalarTowers
 
-variable (Γ : Subgroup (SpecialLinearGroup (Fin 2) ℤ))
-
 instance SLAction {R : Type*} [CommRing R] [Algebra R ℝ] : MulAction SL(2, R) ℍ :=
   MulAction.compHom ℍ <| SpecialLinearGroup.toGLPos.comp <| map (algebraMap R ℝ)
 #align upper_half_plane.SL_action UpperHalfPlane.SLAction
 
+namespace ModularGroup
+
+variable (Γ : Subgroup (SpecialLinearGroup (Fin 2) ℤ))
+
+/-- Canonical embedding of `SL(2, ℤ)` into `GL(2, ℝ)⁺`. -/
 @[coe]
 def coe' : SL(2, ℤ) → GL(2, ℝ)⁺ := fun g => ((g : SL(2, ℝ)) : GL(2, ℝ)⁺)
 
@@ -306,50 +309,52 @@ theorem det_coe' : det (Units.val <| Subtype.val <| coe' g) = 1 := by
 
 instance SLOnGLPos : SMul SL(2, ℤ) GL(2, ℝ)⁺ :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.SL_on_GL_pos UpperHalfPlane.SLOnGLPos
+#align upper_half_plane.SL_on_GL_pos UpperHalfPlane.ModularGroup.SLOnGLPos
 
 theorem SLOnGLPos_smul_apply (s : SL(2, ℤ)) (g : GL(2, ℝ)⁺) (z : ℍ) :
     (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
   rfl
-#align upper_half_plane.SL_on_GL_pos_smul_apply UpperHalfPlane.SLOnGLPos_smul_apply
+#align upper_half_plane.SL_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply
 
 instance SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ where
   smul_assoc := by
     intro s g z
     simp only [SLOnGLPos_smul_apply]
     apply mul_smul'
-#align upper_half_plane.SL_to_GL_tower UpperHalfPlane.SL_to_GL_tower
+#align upper_half_plane.SL_to_GL_tower UpperHalfPlane.ModularGroup.SL_to_GL_tower
 
 instance subgroupGLPos : SMul Γ GL(2, ℝ)⁺ :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.subgroup_GL_pos UpperHalfPlane.subgroupGLPos
+#align upper_half_plane.subgroup_GL_pos UpperHalfPlane.ModularGroup.subgroupGLPos
 
 theorem subgroup_on_glpos_smul_apply (s : Γ) (g : GL(2, ℝ)⁺) (z : ℍ) :
     (s • g) • z = ((s : GL(2, ℝ)⁺) * g) • z :=
   rfl
-#align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.subgroup_on_glpos_smul_apply
+#align upper_half_plane.subgroup_on_GL_pos_smul_apply UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply
 
 instance subgroup_on_glpos : IsScalarTower Γ GL(2, ℝ)⁺ ℍ where
   smul_assoc := by
     intro s g z
     simp only [subgroup_on_glpos_smul_apply]
     apply mul_smul'
-#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.subgroup_on_glpos
+#align upper_half_plane.subgroup_on_GL_pos UpperHalfPlane.ModularGroup.subgroup_on_glpos
 
 instance subgroupSL : SMul Γ SL(2, ℤ) :=
   ⟨fun s g => s * g⟩
-#align upper_half_plane.subgroup_SL UpperHalfPlane.subgroupSL
+#align upper_half_plane.subgroup_SL UpperHalfPlane.ModularGroup.subgroupSL
 
 theorem subgroup_on_SL_apply (s : Γ) (g : SL(2, ℤ)) (z : ℍ) :
     (s • g) • z = ((s : SL(2, ℤ)) * g) • z :=
   rfl
-#align upper_half_plane.subgroup_on_SL_apply UpperHalfPlane.subgroup_on_SL_apply
+#align upper_half_plane.subgroup_on_SL_apply UpperHalfPlane.ModularGroup.subgroup_on_SL_apply
 
 instance subgroup_to_SL_tower : IsScalarTower Γ SL(2, ℤ) ℍ where
   smul_assoc s g z := by
     rw [subgroup_on_SL_apply]
     apply MulAction.mul_smul
-#align upper_half_plane.subgroup_to_SL_tower UpperHalfPlane.subgroup_to_SL_tower
+#align upper_half_plane.subgroup_to_SL_tower UpperHalfPlane.ModularGroup.subgroup_to_SL_tower
+
+end ModularGroup
 
 end ModularScalarTowers
 
@@ -383,6 +388,15 @@ theorem im_smul_eq_div_normSq (g : GL(2, ℝ)⁺) (z : ℍ) :
   smulAux'_im g z
 #align upper_half_plane.im_smul_eq_div_norm_sq UpperHalfPlane.im_smul_eq_div_normSq
 
+theorem c_mul_im_sq_le_normSq_denom (z : ℍ) (g : SL(2, ℝ)) :
+    ((↑ₘg 1 0 : ℝ) * z.im) ^ 2 ≤ Complex.normSq (denom g z) := by
+  let c := (↑ₘg 1 0 : ℝ)
+  let d := (↑ₘg 1 1 : ℝ)
+  calc
+    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
+    _ = Complex.normSq (denom g z) := by dsimp [denom, Complex.normSq]; ring
+#align upper_half_plane.c_mul_im_sq_le_norm_sq_denom UpperHalfPlane.c_mul_im_sq_le_normSq_denom
+
 @[simp]
 theorem neg_smul (g : GL(2, ℝ)⁺) (z : ℍ) : -g • z = g • z := by
   ext1
@@ -394,47 +408,42 @@ theorem neg_smul (g : GL(2, ℝ)⁺) (z : ℍ) : -g • z = g • z := by
 
 section SLModularAction
 
+namespace ModularGroup
+
 variable (g : SL(2, ℤ)) (z : ℍ) (Γ : Subgroup SL(2, ℤ))
 
 @[simp]
 theorem sl_moeb (A : SL(2, ℤ)) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
   rfl
-#align upper_half_plane.sl_moeb UpperHalfPlane.sl_moeb
+#align upper_half_plane.sl_moeb UpperHalfPlane.ModularGroup.sl_moeb
 
 theorem subgroup_moeb (A : Γ) (z : ℍ) : A • z = (A : GL(2, ℝ)⁺) • z :=
   rfl
-#align upper_half_plane.subgroup_moeb UpperHalfPlane.subgroup_moeb
+#align upper_half_plane.subgroup_moeb UpperHalfPlane.ModularGroup.subgroup_moeb
 
 @[simp]
 theorem subgroup_to_sl_moeb (A : Γ) (z : ℍ) : A • z = (A : SL(2, ℤ)) • z :=
   rfl
-#align upper_half_plane.subgroup_to_sl_moeb UpperHalfPlane.subgroup_to_sl_moeb
+#align upper_half_plane.subgroup_to_sl_moeb UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb
 
 @[simp high]
 theorem SL_neg_smul (g : SL(2, ℤ)) (z : ℍ) : -g • z = g • z := by
   simp only [coe_GLPos_neg, sl_moeb, coe_int_neg, neg_smul, coe']
-#align upper_half_plane.SL_neg_smul UpperHalfPlane.SL_neg_smul
+#align upper_half_plane.SL_neg_smul UpperHalfPlane.ModularGroup.SL_neg_smul
 
-theorem c_mul_im_sq_le_normSq_denom (z : ℍ) (g : SL(2, ℝ)) :
-    ((↑ₘg 1 0 : ℝ) * z.im) ^ 2 ≤ Complex.normSq (denom g z) := by
-  let c := (↑ₘg 1 0 : ℝ)
-  let d := (↑ₘg 1 1 : ℝ)
-  calc
-    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
-    _ = Complex.normSq (denom g z) := by dsimp [denom, Complex.normSq]; ring
-#align upper_half_plane.c_mul_im_sq_le_norm_sq_denom UpperHalfPlane.c_mul_im_sq_le_normSq_denom
-
-nonrec theorem SpecialLinearGroup.im_smul_eq_div_normSq :
+nonrec theorem im_smul_eq_div_normSq :
     (g • z).im = z.im / Complex.normSq (denom g z) := by
   convert im_smul_eq_div_normSq g z
   simp only [GeneralLinearGroup.val_det_apply, coe_GLPos_coe_GL_coe_matrix,
     Int.coe_castRingHom, (g : SL(2, ℝ)).prop, one_mul, coe']
-#align upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq
+#align upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq UpperHalfPlane.ModularGroup.im_smul_eq_div_normSq
 
 theorem denom_apply (g : SL(2, ℤ)) (z : ℍ) :
     denom g z = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 * z + (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1 := by
   simp [denom, coe']
-#align upper_half_plane.denom_apply UpperHalfPlane.denom_apply
+#align upper_half_plane.denom_apply UpperHalfPlane.ModularGroup.denom_apply
+
+end ModularGroup
 
 end SLModularAction
 

Mathlib/NumberTheory/Modular.lean

@@ -65,7 +65,7 @@ open Complex hiding abs_two
 
 open Matrix hiding mul_smul
 
-open Matrix.SpecialLinearGroup UpperHalfPlane
+open Matrix.SpecialLinearGroup UpperHalfPlane ModularGroup
 
 noncomputable section
 
@@ -289,7 +289,7 @@ theorem exists_max_im : ∃ g : SL(2, ℤ), ∀ g' : SL(2, ℤ), (g' • z).im 
     Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)
   obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime
   refine' ⟨g, fun g' => _⟩
-  rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq,
+  rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
     div_le_div_left]
   · simpa [← hg] using hp ((↑ₘg') 1) (bottom_row_coprime g')
   · exact z.im_pos
@@ -380,7 +380,7 @@ theorem im_lt_im_S_smul (h : normSq z < 1) : z.im < (S • z).im := by
     apply (lt_div_iff z.normSq_pos).mpr
     nlinarith
   convert this
-  simp only [SpecialLinearGroup.im_smul_eq_div_normSq]
+  simp only [ModularGroup.im_smul_eq_div_normSq]
   simp [denom, coe_S]
 #align modular_group.im_lt_im_S_smul ModularGroup.im_lt_im_S_smul
 
@@ -445,7 +445,7 @@ theorem exists_smul_mem_fd (z : ℍ) : ∃ g : SL(2, ℤ), g • z ∈ 𝒟 := b
   -- `g` has same max im property as `g₀`
   have hg₀' : ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
     have hg'' : (g • z).im = (g₀ • z).im := by
-      rw [SpecialLinearGroup.im_smul_eq_div_normSq, SpecialLinearGroup.im_smul_eq_div_normSq,
+      rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
         denom_apply, denom_apply, hg]
     simpa only [hg''] using hg₀
   constructor
@@ -500,7 +500,7 @@ theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |(↑ₘg
   calc
     9 * c ^ 4 < c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
     _ = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16 := by
-      rw [SpecialLinearGroup.im_smul_eq_div_normSq, div_pow]
+      rw [ModularGroup.im_smul_eq_div_normSq, div_pow]
       ring
     _ ≤ 16 := by rw [← mul_pow]; linarith
 #align modular_group.abs_c_le_one ModularGroup.abs_c_le_one

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

@@ -109,9 +109,9 @@ def eisensteinSeries (k : ℤ) (z : ℍ) : ℂ := ∑' x : gammaSet N a, eisSumm
 lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
     eisensteinSeries a k ∣[k] γ = eisensteinSeries (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]
+  simp_rw [SL_slash, slash_def, slash, ModularGroup.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, ← ModularGroup.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)`,

Mathlib/NumberTheory/ModularForms/SlashActions.lean

@@ -25,7 +25,7 @@ In the `ModularForm` locale, this provides
 -/
 
 
-open Complex UpperHalfPlane
+open Complex UpperHalfPlane ModularGroup
 
 open scoped UpperHalfPlane