feat(analysis/complex/upper_half_plane/metric): prove that SL(2, ℝ) acts isometrically on upper half space with the hyperbolic metric (#18379)

RuizheWan · ocfnash · eric-wieser · RuizheWan · commit f06058e64b7e · 2023-03-01T21:21:22.000Z
A key part of the argument is to show that the element `modular_group.S` acts isometrically. We thus move the definition `modular_group.S` (and its partner `modular_group.T`) earlier in the import hierarchy to make it available without introducing a dependency on the theory of the modular group.



Co-authored-by: Oliver Nash &lt;github@olivernash.org&gt;
Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
Co-authored-by: RuizheWan &lt;115158055+RuizheWan@users.noreply.github.com&gt;
diff --git a/src/analysis/complex/upper_half_plane/basic.lean b/src/analysis/complex/upper_half_plane/basic.lean
@@ -8,7 +8,7 @@ import linear_algebra.matrix.special_linear_group
 import analysis.complex.basic
 import group_theory.group_action.defs
 import linear_algebra.matrix.general_linear_group
-
+import tactic.linear_combination
 
 /-!
 # The upper half plane and its automorphisms
@@ -30,11 +30,13 @@ open_locale classical big_operators matrix_groups
 
 local attribute [instance] fintype.card_fin_even
 
-/- Disable this instances as it is not the simp-normal form, and having them disabled ensures
+/- Disable these instances as they are not the simp-normal form, and having them disabled ensures
 we state lemmas in this file without spurious `coe_fn` terms. -/
 local attribute [-instance] matrix.special_linear_group.has_coe_to_fun
+local attribute [-instance] matrix.general_linear_group.has_coe_to_fun
 
 local prefix `↑ₘ`:1024 := @coe _ (matrix (fin 2) (fin 2) _) _
+local notation `↑ₘ[`:1024 R `]` := @coe _ (matrix (fin 2) (fin 2) R) _
 
 local notation `GL(` n `, ` R `)`⁺ := matrix.GL_pos (fin n) R
 
@@ -84,6 +86,9 @@ by { rw complex.norm_sq_pos, exact z.ne_zero }
 
 lemma norm_sq_ne_zero (z : ℍ) : complex.norm_sq (z : ℂ) ≠ 0 := (norm_sq_pos z).ne'
 
+lemma im_inv_neg_coe_pos (z : ℍ) : 0 < ((-z : ℂ)⁻¹).im :=
+by simpa using div_pos z.property (norm_sq_pos z)
+
 /-- Numerator of the formula for a fractional linear transformation -/
 @[simp] def num (g : GL(2, ℝ)⁺) (z : ℍ) : ℂ := (↑ₘg 0 0 : ℝ) * z + (↑ₘg 0 1 : ℝ)
 
@@ -217,6 +222,11 @@ instance subgroup_to_SL_tower : is_scalar_tower Γ SL(2,ℤ) ℍ :=
 
 end modular_scalar_towers
 
+lemma special_linear_group_apply {R : Type*} [comm_ring R] [algebra R ℝ] (g : SL(2, R)) (z : ℍ) :
+  g • z = mk ((((↑(↑ₘ[R] g 0 0) : ℝ) : ℂ) * z + ((↑(↑ₘ[R] g 0 1) : ℝ) : ℂ)) /
+              (((↑(↑ₘ[R] g 1 0) : ℝ) : ℂ) * z + ((↑(↑ₘ[R] g 1 1) : ℝ) : ℂ))) (g • z).property :=
+rfl
+
 @[simp] lemma coe_smul (g : GL(2, ℝ)⁺) (z : ℍ) : ↑(g • z) = num g z / denom g z := rfl
 @[simp] lemma re_smul (g : GL(2, ℝ)⁺) (z : ℍ) : (g • z).re = (num g z / denom g z).re := rfl
 lemma im_smul (g : GL(2, ℝ)⁺) (z : ℍ) : (g • z).im = (num g z / denom g z).im := rfl
@@ -299,4 +309,40 @@ variables (x : ℝ) (z : ℍ)
 
 end real_add_action
 
+@[simp] lemma modular_S_smul (z : ℍ) : modular_group.S • z = mk (-z : ℂ)⁻¹ z.im_inv_neg_coe_pos :=
+by { rw special_linear_group_apply, simp [modular_group.S, neg_div, inv_neg], }
+
+lemma exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : SL(2, ℝ)) (hc : ↑ₘ[ℝ] g 1 0 = 0) :
+  ∃ (u : {x : ℝ // 0 < x}) (v : ℝ),
+    ((•) g : ℍ → ℍ) = (λ z, v +ᵥ z) ∘ (λ z, u • z) :=
+begin
+  obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc,
+  refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, _⟩,
+  ext1 ⟨z, hz⟩, ext1,
+  suffices : ↑a * z * a + b * a = b * a + a * a * z,
+  { rw special_linear_group_apply, simpa [add_mul], },
+  ring,
+end
+
+lemma exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : SL(2, ℝ)) (hc : ↑ₘ[ℝ] g 1 0 ≠ 0) :
+  ∃ (u : {x : ℝ // 0 < x}) (v w : ℝ),
+    ((•) g : ℍ → ℍ) = ((+ᵥ) w : ℍ → ℍ) ∘ ((•) modular_group.S : ℍ → ℍ)
+                     ∘ ((+ᵥ) v : ℍ → ℍ) ∘ ((•) u : ℍ → ℍ) :=
+begin
+  have h_denom := denom_ne_zero g,
+  induction g using matrix.special_linear_group.fin_two_induction with a b c d h,
+  replace hc : c ≠ 0, { simpa using hc, },
+  refine ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, _⟩,
+  ext1 ⟨z, hz⟩, ext1,
+  suffices : (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹,
+  { rw special_linear_group_apply, simpa [-neg_add_rev, inv_neg, ← sub_eq_add_neg], },
+  replace hc : (c : ℂ) ≠ 0, { norm_cast, assumption, },
+  replace h_denom : ↑c * z + d ≠ 0, { simpa using h_denom ⟨z, hz⟩, },
+  have h_aux : (c : ℂ) * d + ↑c * ↑c * z ≠ 0,
+  { rw [mul_assoc, ← mul_add, add_comm], exact mul_ne_zero hc h_denom, },
+  replace h : (a * d - b * c : ℂ) = (1 : ℂ), { norm_cast, assumption, },
+  field_simp,
+  linear_combination (-(z * ↑c ^ 2) - ↑c * ↑d) * h,
+end
+
 end upper_half_plane
diff --git a/src/analysis/complex/upper_half_plane/metric.lean b/src/analysis/complex/upper_half_plane/metric.lean
@@ -24,7 +24,7 @@ ball/sphere with another center and radius.
 
 noncomputable theory
 
-open_locale upper_half_plane complex_conjugate nnreal topology
+open_locale upper_half_plane complex_conjugate nnreal topology matrix_groups
 open set metric filter real
 
 variables {z w : ℍ} {r R : ℝ}
@@ -349,4 +349,26 @@ begin
   exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')
 end
 
+/-- `SL(2, ℝ)` acts on the upper half plane as an isometry.-/
+instance : has_isometric_smul SL(2, ℝ) ℍ :=
+⟨λ g,
+begin
+  have h₀ : isometry (λ z, modular_group.S • z : ℍ → ℍ) := isometry.of_dist_eq (λ y₁ y₂, by
+  { have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le,
+    have h₂ : complex.abs (y₁ * y₂) ≠ 0, { simp [y₁.ne_zero, y₂.ne_zero], },
+    simp only [dist_eq, modular_S_smul, inv_neg, neg_div, div_mul_div_comm, coe_mk, mk_im, div_one,
+      complex.inv_im, complex.neg_im, coe_im, neg_neg, complex.norm_sq_neg, mul_eq_mul_left_iff,
+      real.arsinh_inj, bit0_eq_zero, one_ne_zero, or_false, dist_neg_neg, mul_neg, neg_mul,
+      dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, ← absolute_value.map_mul,
+      ← complex.norm_sq_mul, real.sqrt_div h₁, ← complex.abs_apply, mul_div (2 : ℝ),
+      div_div_div_comm, div_self h₂, complex.norm_eq_abs], }),
+  by_cases hc : g 1 0 = 0,
+  { obtain ⟨u, v, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_eq_zero g hc,
+    rw h,
+    exact (isometry_real_vadd v).comp (isometry_pos_mul u), },
+  { obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc,
+    rw h,
+    exact (isometry_real_vadd w).comp (h₀.comp $ (isometry_real_vadd v).comp $ isometry_pos_mul u) }
+end⟩
+
 end upper_half_plane
diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean
@@ -474,6 +474,15 @@ nnreal.eq $ by simp
 @[simp] lemma nnnorm_zpow : ∀ (a : α) (n : ℤ), ‖a ^ n‖₊ = ‖a‖₊ ^ n :=
 map_zpow₀ (nnnorm_hom : α →*₀ ℝ≥0)
 
+lemma dist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
+  dist z⁻¹ w⁻¹ = (dist z w) / (‖z‖ * ‖w‖) :=
+by rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
+  mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
+
+lemma nndist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
+  nndist z⁻¹ w⁻¹ = (nndist z w) / (‖z‖₊ * ‖w‖₊) :=
+by { rw ← nnreal.coe_eq, simp [-nnreal.coe_eq, dist_inv_inv₀ hz hw], }
+
 /-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
 infinity. TODO: use `bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/
 lemma filter.tendsto_mul_left_cobounded {a : α} (ha : a ≠ 0) :
diff --git a/src/linear_algebra/matrix/special_linear_group.lean b/src/linear_algebra/matrix/special_linear_group.lean
@@ -232,6 +232,27 @@ begin
   refl,
 end
 
+lemma fin_two_induction (P : SL(2, R) → Prop)
+  (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], by rwa [det_fin_two_of]⟩)
+  (g : SL(2, R)) : P g :=
+begin
+  obtain ⟨m, hm⟩ := g,
+  convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa det_fin_two at hm),
+  ext i j, fin_cases i; fin_cases j; refl,
+end
+
+lemma fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type*} [field R]
+  (g : SL(2, R)) (hg : (g : matrix (fin 2) (fin 2) R) 1 0 = 0) :
+  ∃ (a b : R) (h : a ≠ 0),
+    g = (⟨!![a, b; 0, a⁻¹], by simp [h]⟩ : SL(2, R)) :=
+begin
+  induction g using matrix.special_linear_group.fin_two_induction with a b c d h_det,
+  replace hg : c = 0 := by simpa using hg,
+  have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det,
+  refine ⟨a, b, left_ne_zero_of_mul_eq_one had, _⟩,
+  simp_rw [eq_inv_of_mul_eq_one_right had, hg],
+end
+
 end special_cases
 
 -- this section should be last to ensure we do not use it in lemmas
@@ -249,3 +270,49 @@ end coe_fn_instance
 end special_linear_group
 
 end matrix
+
+namespace modular_group
+
+open_locale matrix_groups
+open matrix matrix.special_linear_group
+
+local prefix `↑ₘ`:1024 := @coe _ (matrix (fin 2) (fin 2) ℤ) _
+
+/-- The matrix `S = [[0, -1], [1, 0]]` as an element of `SL(2, ℤ)`.
+
+This element acts naturally on the Euclidean plane as a rotation about the origin by `π / 2`.
+
+This element also acts naturally on the hyperbolic plane as rotation about `i` by `π`. It
+represents the Mobiüs transformation `z ↦ -1/z` and is an involutive elliptic isometry. -/
+def S : SL(2, ℤ) := ⟨!![0, -1; 1, 0], by norm_num [matrix.det_fin_two_of]⟩
+
+/-- The matrix `T = [[1, 1], [0, 1]]` as an element of `SL(2, ℤ)` -/
+def T : SL(2, ℤ) := ⟨!![1, 1; 0, 1], by norm_num [matrix.det_fin_two_of]⟩
+
+lemma coe_S : ↑ₘS = !![0, -1; 1, 0] := rfl
+
+lemma coe_T : ↑ₘT = !![1, 1; 0, 1] := rfl
+
+lemma coe_T_inv : ↑ₘ(T⁻¹) = !![1, -1; 0, 1] := by simp [coe_inv, coe_T, adjugate_fin_two]
+
+lemma coe_T_zpow (n : ℤ) : ↑ₘ(T ^ n) = !![1, n; 0, 1] :=
+begin
+  induction n using int.induction_on with n h n h,
+  { rw [zpow_zero, coe_one, matrix.one_fin_two] },
+  { simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, matrix.mul_fin_two],
+    congrm !![_, _; _, _],
+    rw [mul_one, mul_one, add_comm] },
+  { simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, matrix.mul_fin_two],
+    congrm !![_, _; _, _]; ring },
+end
+
+@[simp] lemma T_pow_mul_apply_one (n : ℤ) (g : SL(2, ℤ)) : ↑ₘ(T ^ n * g) 1 = ↑ₘg 1 :=
+by simp [coe_T_zpow, matrix.mul, matrix.dot_product, fin.sum_univ_succ]
+
+@[simp] lemma T_mul_apply_one (g : SL(2, ℤ)) : ↑ₘ(T * g) 1 = ↑ₘg 1 :=
+by simpa using T_pow_mul_apply_one 1 g
+
+@[simp] lemma T_inv_mul_apply_one (g : SL(2, ℤ)) : ↑ₘ(T⁻¹ * g) 1 = ↑ₘg 1 :=
+by simpa using T_pow_mul_apply_one (-1) g
+
+end modular_group
diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean
@@ -314,38 +314,6 @@ begin
     exact hg ⟨g1, this⟩ },
 end
 
-/-- The matrix `T = [[1,1],[0,1]]` as an element of `SL(2,ℤ)` -/
-def T : SL(2,ℤ) := ⟨!![1, 1; 0, 1], by norm_num [matrix.det_fin_two_of]⟩
-
-/-- The matrix `S = [[0,-1],[1,0]]` as an element of `SL(2,ℤ)` -/
-def S : SL(2,ℤ) := ⟨!![0, -1; 1, 0], by norm_num [matrix.det_fin_two_of]⟩
-
-lemma coe_S : ↑ₘS = !![0, -1; 1, 0] := rfl
-
-lemma coe_T : ↑ₘT = !![1, 1; 0, 1] := rfl
-
-lemma coe_T_inv : ↑ₘ(T⁻¹) = !![1, -1; 0, 1] := by simp [coe_inv, coe_T, adjugate_fin_two]
-
-lemma coe_T_zpow (n : ℤ) : ↑ₘ(T ^ n) = !![1, n; 0, 1] :=
-begin
-  induction n using int.induction_on with n h n h,
-  { rw [zpow_zero, coe_one, matrix.one_fin_two] },
-  { simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, matrix.mul_fin_two],
-    congrm !![_, _; _, _],
-    rw [mul_one, mul_one, add_comm] },
-  { simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, matrix.mul_fin_two],
-    congrm !![_, _; _, _]; ring },
-end
-
-@[simp] lemma T_pow_mul_apply_one (n : ℤ) (g : SL(2, ℤ)) : ↑ₘ(T ^ n * g) 1 = ↑ₘg 1 :=
-by simp [coe_T_zpow, matrix.mul, matrix.dot_product, fin.sum_univ_succ]
-
-@[simp] lemma T_mul_apply_one (g : SL(2, ℤ)) : ↑ₘ(T * g) 1 = ↑ₘg 1 :=
-by simpa using T_pow_mul_apply_one 1 g
-
-@[simp] lemma T_inv_mul_apply_one (g : SL(2, ℤ)) : ↑ₘ(T⁻¹ * g) 1 = ↑ₘg 1 :=
-by simpa using T_pow_mul_apply_one (-1) g
-
 lemma coe_T_zpow_smul_eq {n : ℤ} : (↑((T^n) • z) : ℂ) = z + n :=
 by simp [coe_T_zpow]
 
