feat(number_theory/modular): the action of SL(2, ℤ) on the upper ha…

…lf plane (#8611)

We define the action of `SL(2,ℤ)` on `ℍ` (via restriction of the `SL(2,ℝ)` action in `analysis.complex.upper_half_plane`). We then define the standard fundamental domain `𝒟` for this action and show that any point in `ℍ` can be moved inside `𝒟`.

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com>

src/linear_algebra/basic.lean

@@ -2645,6 +2645,10 @@ def general_linear_equiv : general_linear_group R M ≃* (M ≃ₗ[R] M) :=
   (general_linear_equiv R M f : M →ₗ[R] M) = f :=
 by {ext, refl}
 
+@[simp] lemma coe_fn_general_linear_equiv (f : general_linear_group R M) :
+  ⇑(general_linear_equiv R M f) = (f : M → M) :=
+rfl
+
 end general_linear_group
 
 end linear_map

src/linear_algebra/general_linear_group.lean

@@ -57,6 +57,11 @@ unit_of_det_invertible A
 noncomputable def mk'' (A : matrix n n R) (h : is_unit (matrix.det A)) : GL n R :=
 nonsing_inv_unit A h
 
+/--Given a matrix with non-zero determinant over a field, we get an element of `GL n K`-/
+def mk_of_det_ne_zero {K : Type*} [field K] (A : matrix n n K) (h : matrix.det A ≠ 0) :
+  GL n K :=
+mk' A (invertible_of_nonzero h)
+
 instance coe_fun : has_coe_to_fun (GL n R) (λ _, n → n → R) :=
 { coe := λ A, A.val }
 
@@ -84,6 +89,23 @@ begin
   exact inv_of_eq_nonsing_inv (↑A : matrix n n R),
 end
 
+/-- An element of the matrix general linear group on `(n) [fintype n]` can be considered as an
+element of the endomorphism general linear group on `n → R`. -/
+def to_linear : general_linear_group n R ≃* linear_map.general_linear_group R (n → R) :=
+units.map_equiv matrix.to_lin_alg_equiv'.to_ring_equiv.to_mul_equiv
+
+-- Note that without the `@` and `‹_›`, lean infers `λ a b, _inst_1 a b` instead of `_inst_1` as the
+-- decidability argument, which prevents `simp` from obtaining the instance by unification.
+-- These `λ a b, _inst a b` terms also appear in the type of `A`, but simp doesn't get confused by
+-- them so for now we do not care.
+@[simp] lemma coe_to_linear :
+  (@to_linear n ‹_› ‹_› _ _ A : (n → R) →ₗ[R] (n → R)) = matrix.mul_vec_lin A :=
+rfl
+
+@[simp] lemma to_linear_apply (v : n → R) :
+  (@to_linear n ‹_› ‹_› _ _ A) v = matrix.mul_vec_lin A v :=
+rfl
+
 end coe_lemmas
 
 end general_linear_group
@@ -164,4 +186,21 @@ lemma to_GL_pos_injective :
  from subtype.coe_injective).of_comp
 
 end special_linear_group
+
+section examples
+
+/-- The matrix [a, b; -b, a] (inspired by multiplication by a complex number); it is an element of
+$GL_2(R)$ if `a ^ 2 + b ^ 2` is nonzero. -/
+@[simps coe {fully_applied := ff}]
+def plane_conformal_matrix {R} [field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) :
+  matrix.general_linear_group (fin 2) R :=
+general_linear_group.mk_of_det_ne_zero ![![a, b], ![-b, a]]
+  (by simpa [det_fin_two, sq] using hab)
+
+/- TODO: Add Iwasawa matrices `n_x=![![1,x],![0,1]]`, `a_t=![![exp(t/2),0],![0,exp(-t/2)]]` and
+  `k_θ==![![cos θ, sin θ],![-sin θ, cos θ]]`
+-/
+
+end examples
+
 end matrix

src/linear_algebra/special_linear_group.lean

@@ -99,6 +99,10 @@ section coe_lemmas
 
 variables (A B : special_linear_group n R)
 
+@[simp] lemma coe_mk (A : matrix n n R) (h : det A = 1) :
+  ↑(⟨A, h⟩ : special_linear_group n R) = A :=
+rfl
+
 @[simp] lemma coe_inv : ↑ₘ(A⁻¹) = adjugate A := rfl
 
 @[simp] lemma coe_mul : ↑ₘ(A * B) = ↑ₘA ⬝ ↑ₘB := rfl
@@ -156,6 +160,28 @@ def to_GL : special_linear_group n R →* general_linear_group R (n → R) :=
 
 lemma coe_to_GL (A : special_linear_group n R) : ↑A.to_GL = A.to_lin'.to_linear_map := rfl
 
+variables {S : Type*} [comm_ring S]
+
+/-- A ring homomorphism from `R` to `S` induces a group homomorphism from
+`special_linear_group n R` to `special_linear_group n S`. -/
+@[simps] def map (f : R →+* S) : special_linear_group n R →* special_linear_group n S :=
+{ to_fun := λ g, ⟨f.map_matrix ↑g, by { rw ← f.map_det, simp [g.2] }⟩,
+  map_one' := subtype.ext $ f.map_matrix.map_one,
+  map_mul' := λ x y, subtype.ext $ f.map_matrix.map_mul x y }
+
+section cast
+
+/-- Coercion of SL `n` `ℤ` to SL `n` `R` for a commutative ring `R`. -/
+instance : has_coe (special_linear_group n ℤ) (special_linear_group n R) :=
+⟨λ x, map (int.cast_ring_hom R) x⟩
+
+@[simp] lemma coe_matrix_coe (g : special_linear_group n ℤ) :
+  ↑(g : special_linear_group n R)
+  = (↑g : matrix n n ℤ).map (int.cast_ring_hom R) :=
+map_apply_coe (int.cast_ring_hom R) g
+
+end cast
+
 section has_neg
 
 variables [fact (even (fintype.card n))]
@@ -171,6 +197,10 @@ instance : has_neg (special_linear_group n R) :=
   ↑(- g) = - (↑g : matrix n n R) :=
 rfl
 
+@[simp] lemma coe_int_neg (g : (special_linear_group n ℤ)) :
+  ↑(-g) = (-↑g : special_linear_group n R) :=
+subtype.ext $ (@ring_hom.map_matrix n _ _ _ _ _ _ (int.cast_ring_hom R)).map_neg ↑g
+
 end has_neg
 
 -- this section should be last to ensure we do not use it in lemmas

src/measure_theory/group/basic.lean

@@ -303,7 +303,7 @@ a right-invariant measure. -/
 lemma lintegral_mul_right_eq_self (hμ : is_mul_right_invariant μ) (f : G → ℝ≥0∞) (g : G) :
   ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ :=
 begin
-  have : measure.map (homeomorph.mul_right g) μ = μ,
+  have : measure.map (λ g', g' * g) μ = μ,
   { rw ← map_mul_right_eq_self at hμ,
     exact hμ g },
   convert (lintegral_map_equiv f (homeomorph.mul_right g).to_measurable_equiv).symm,