feat(NumberTheory/Modular): strengthen 2nd Fundamental-Domain Lemma (leanprover-community#36736)

Strengthen the results on the fundamental domain for the modular group, by proving that the interior of the fundamental domain is disjoint from any translate of the fundamental domain.

Proof closely follows Serre _A Course in Arithmetic_ (although Serre also proves that S, T generate the modular group at the same time, which we do not do, since this is proved by a different method in `FixedDetMatrices`).

Author: loefflerd

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -29,17 +29,26 @@ structure UpperHalfPlane where
 
 @[inherit_doc] scoped[UpperHalfPlane] notation "ℍ" => UpperHalfPlane
 
-open UpperHalfPlane
+open UpperHalfPlane Complex
 
 namespace UpperHalfPlane
 
 attribute [coe] UpperHalfPlane.coe
 
 instance : CoeOut ℍ ℂ := ⟨UpperHalfPlane.coe⟩
 
-/-- Define I := √-1 as an element on the upper half plane. -/
+/-- Define `I := √-1` as an element of the upper half plane. -/
 def I : ℍ := ⟨Complex.I, zero_lt_one⟩
 
+/-- Define the cube root of unity `ρ := (-1 + √-3) / 2` as an element of the upper half plane. -/
+def ρ : ℍ := ⟨⟨-1 / 2, Real.sqrt 3 / 2⟩, by positivity⟩
+
+lemma ρ_sq : (ρ : ℂ) ^ 2 = -ρ - 1 := by
+  simp [Complex.ext_iff, pow_two, ρ]
+  grind
+
+lemma norm_ρ : ‖(ρ : ℂ)‖ = 1 := by norm_num [norm_def, normSq, ← pow_two, ρ, div_pow]
+
 instance : Inhabited ℍ := ⟨.I⟩
 
 @[simp, norm_cast] theorem coe_inj {a b : ℍ} : (a : ℂ) = b ↔ a = b := UpperHalfPlane.ext_iff.symm
@@ -123,6 +132,14 @@ theorem ne_zero (z : ℍ) : (z : ℂ) ≠ 0 :=
 lemma mem_slitPlane (z : ℍ) : (z : ℂ) ∈ Complex.slitPlane := by
   simp [Complex.slitPlane, im_ne_zero z]
 
+/-- Criterion for equality in terms of real part and norm. Useful when working with the
+geometry of the fundamental domain. -/
+lemma eq_of_re_of_norm {τ τ' : ℍ} (hre : τ.re = τ'.re) (hnorm : ‖(τ : ℂ)‖ = ‖(τ' : ℂ)‖) :
+    τ = τ' := by
+  apply_fun (· ^ 2) at hnorm
+  simpa [UpperHalfPlane.ext_iff, Complex.ext_iff, hre, Complex.normSq, Complex.sq_norm,
+    ← pow_two, pow_left_inj₀ τ.im_pos.le τ'.im_pos.le two_ne_zero] using hnorm
+
 end UpperHalfPlane
 
 namespace Mathlib.Meta.Positivity

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

@@ -6,7 +6,6 @@ Authors: Alex Kontorovich, Heather Macbeth, Marc Masdeu
 module
 
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
-public import Mathlib.Data.Fintype.Parity
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 
 /-!

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen, Wen Yang
 -/
 module
 
+public import Mathlib.Data.Fintype.Parity
 public import Mathlib.LinearAlgebra.Matrix.Adjugate
 public import Mathlib.LinearAlgebra.Matrix.ToLin
 public import Mathlib.LinearAlgebra.Matrix.Transvection
@@ -77,6 +78,9 @@ namespace SpecialLinearGroup
 
 variable {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R]
 
+/-- If `R` and `n` have decidable equality then so does `SL(n, R)`. -/
+instance [DecidableEq R] : DecidableEq (SpecialLinearGroup n R) := Subtype.instDecidableEq
+
 instance hasCoeToMatrix : Coe (SpecialLinearGroup n R) (Matrix n n R) :=
   ⟨fun A => A.val⟩
 
@@ -479,6 +483,8 @@ def T : SL(2, ℤ) :=
 theorem coe_S : ↑S = !![0, -1; 1, 0] :=
   rfl
 
+lemma S_inv : S⁻¹ = -S := by decide
+
 theorem coe_T : ↑T = (!![1, 1; 0, 1] : Matrix _ _ ℤ) :=
   rfl