From 9c4e41aea85ee16790b16e6da0acf3a65d9771e3 Mon Sep 17 00:00:00 2001 From: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com> Date: Sat, 4 Dec 2021 05:05:06 +0000 Subject: [PATCH] =?UTF-8?q?feat(number=5Ftheory/modular):=20the=20action?= =?UTF-8?q?=20of=20`SL(2,=20=E2=84=A4)`=20on=20the=20upper=20half=20plane?= =?UTF-8?q?=20(#8611)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Marc Masdeu --- src/linear_algebra/basic.lean | 4 + src/linear_algebra/general_linear_group.lean | 39 ++ src/linear_algebra/special_linear_group.lean | 30 ++ src/measure_theory/group/basic.lean | 2 +- src/number_theory/modular.lean | 377 +++++++++++++++++++ src/topology/algebra/group.lean | 8 + src/topology/homeomorph.lean | 2 + 7 files changed, 461 insertions(+), 1 deletion(-) create mode 100644 src/number_theory/modular.lean diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 779659882af26..f73ac49d05c5c 100644 --- a/src/linear_algebra/basic.lean +++ b/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 diff --git a/src/linear_algebra/general_linear_group.lean b/src/linear_algebra/general_linear_group.lean index 96125d62f4874..50672bb9da7f1 100644 --- a/src/linear_algebra/general_linear_group.lean +++ b/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 diff --git a/src/linear_algebra/special_linear_group.lean b/src/linear_algebra/special_linear_group.lean index bb19317475e93..19fddad4a1fcd 100644 --- a/src/linear_algebra/special_linear_group.lean +++ b/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 diff --git a/src/measure_theory/group/basic.lean b/src/measure_theory/group/basic.lean index bc875ca448262..fcc5b1459897a 100644 --- a/src/measure_theory/group/basic.lean +++ b/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, diff --git a/src/number_theory/modular.lean b/src/number_theory/modular.lean new file mode 100644 index 0000000000000..cafa1dddb0cac --- /dev/null +++ b/src/number_theory/modular.lean @@ -0,0 +1,377 @@ +/- +Copyright (c) 2021 Alex Kontorovich and Heather Macbeth and Marc Masdeu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex Kontorovich, Heather Macbeth, Marc Masdeu +-/ + +import analysis.complex.upper_half_plane +import linear_algebra.general_linear_group + +/-! +# The action of the modular group SL(2, β„€) on the upper half-plane + +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 +(`modular_group.fundamental_domain`, `π’Ÿ`) for this action and show +(`modular_group.exists_smul_mem_fundamental_domain`) that any point in `ℍ` can be +moved inside `π’Ÿ`. + +Standard proofs make use of the identity + +`g β€’ z = a / c - 1 / (c (cz + d))` + +for `g = [[a, b], [c, d]]` in `SL(2)`, but this requires separate handling of whether `c = 0`. +Instead, our proof makes use of the following perhaps novel identity (see +`modular_group.smul_eq_lc_row0_add`): + +`g β€’ z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))` + +where there is no issue of division by zero. + +Another feature is that we delay until the very end the consideration of special matrices +`T=[[1,1],[0,1]]` (see `modular_group.T`) and `S=[[0,-1],[1,0]]` (see `modular_group.S`), by +instead using abstract theory on the properness of certain maps (phrased in terms of the filters +`filter.cocompact`, `filter.cofinite`, etc) to deduce existence theorems, first to prove the +existence of `g` maximizing `(gβ€’z).im` (see `modular_group.exists_max_im`), and then among +those, to minimize `|(gβ€’z).re|` (see `modular_group.exists_row_one_eq_and_min_re`). +-/ + +open complex matrix matrix.special_linear_group upper_half_plane +noncomputable theory + +local notation `SL(` n `, ` R `)`:= special_linear_group (fin n) R +local prefix `β†‘β‚˜`:1024 := @coe _ (matrix (fin 2) (fin 2) β„€) _ + + +open_locale upper_half_plane complex_conjugate + +local attribute [instance] fintype.card_fin_even + +namespace modular_group + +section upper_half_plane_action + +/-- For a subring `R` of `ℝ`, the action of `SL(2, R)` on the upper half-plane, as a restriction of +the `SL(2, ℝ)`-action defined by `upper_half_plane.mul_action`. -/ +instance {R : Type*} [comm_ring R] [algebra R ℝ] : mul_action SL(2, R) ℍ := +mul_action.comp_hom ℍ (map (algebra_map R ℝ)) + +lemma coe_smul (g : SL(2, β„€)) (z : ℍ) : ↑(g β€’ z) = num g z / denom g z := rfl +lemma re_smul (g : SL(2, β„€)) (z : ℍ) : (g β€’ z).re = (num g z / denom g z).re := rfl +@[simp] lemma smul_coe (g : SL(2, β„€)) (z : ℍ) : (g : SL(2,ℝ)) β€’ z = g β€’ z := rfl + +@[simp] lemma neg_smul (g : SL(2, β„€)) (z : ℍ) : -g β€’ z = g β€’ z := +show ↑(-g) β€’ _ = _, by simp [neg_smul g z] + +lemma im_smul (g : SL(2, β„€)) (z : ℍ) : (g β€’ z).im = (num g z / denom g z).im := rfl + +lemma im_smul_eq_div_norm_sq (g : SL(2, β„€)) (z : ℍ) : + (g β€’ z).im = z.im / (complex.norm_sq (denom g z)) := +im_smul_eq_div_norm_sq g z + +@[simp] lemma denom_apply (g : SL(2, β„€)) (z : ℍ) : denom g z = β†‘β‚˜g 1 0 * z + β†‘β‚˜g 1 1 := by simp + +end upper_half_plane_action + +section bottom_row + +/-- The two numbers `c`, `d` in the "bottom_row" of `g=[[*,*],[c,d]]` in `SL(2, β„€)` are coprime. -/ +lemma bottom_row_coprime {R : Type*} [comm_ring R] (g : SL(2, R)) : + is_coprime ((↑g : matrix (fin 2) (fin 2) R) 1 0) ((↑g : matrix (fin 2) (fin 2) R) 1 1) := +begin + use [- (↑g : matrix (fin 2) (fin 2) R) 0 1, (↑g : matrix (fin 2) (fin 2) R) 0 0], + rw [add_comm, ←neg_mul_eq_neg_mul, ←sub_eq_add_neg, ←det_fin_two], + exact g.det_coe, +end + +/-- Every pair `![c, d]` of coprime integers is the "bottom_row" of some element `g=[[*,*],[c,d]]` +of `SL(2,β„€)`. -/ +lemma bottom_row_surj {R : Type*} [comm_ring R] : + set.surj_on (Ξ» g : SL(2, R), @coe _ (matrix (fin 2) (fin 2) R) _ g 1) set.univ + {cd | is_coprime (cd 0) (cd 1)} := +begin + rintros cd ⟨bβ‚€, a, gcd_eqn⟩, + let A := ![![a, -bβ‚€], cd], + have det_A_1 : det A = 1, + { convert gcd_eqn, + simp [A, det_fin_two, (by ring : a * (cd 1) + bβ‚€ * (cd 0) = bβ‚€ * (cd 0) + a * (cd 1))] }, + refine ⟨⟨A, det_A_1⟩, set.mem_univ _, _⟩, + ext; simp [A] +end + +end bottom_row + +section tendsto_lemmas + +open filter continuous_linear_map +local attribute [instance] matrix.normed_group matrix.normed_space +local attribute [simp] coe_smul + +/-- The function `(c,d) β†’ |cz+d|^2` is proper, that is, preimages of bounded-above sets are finite. +-/ +lemma tendsto_norm_sq_coprime_pair (z : ℍ) : + filter.tendsto (Ξ» p : fin 2 β†’ β„€, ((p 0 : β„‚) * z + p 1).norm_sq) + cofinite at_top := +begin + let Ο€β‚€ : (fin 2 β†’ ℝ) β†’β‚—[ℝ] ℝ := linear_map.proj 0, + let π₁ : (fin 2 β†’ ℝ) β†’β‚—[ℝ] ℝ := linear_map.proj 1, + let f : (fin 2 β†’ ℝ) β†’β‚—[ℝ] β„‚ := Ο€β‚€.smul_right (z:β„‚) + π₁.smul_right 1, + have f_def : ⇑f = Ξ» (p : fin 2 β†’ ℝ), (p 0 : β„‚) * ↑z + p 1, + { ext1, + dsimp only [linear_map.coe_proj, real_smul, + linear_map.coe_smul_right, linear_map.add_apply], + rw mul_one, }, + have : (Ξ» (p : fin 2 β†’ β„€), norm_sq ((p 0 : β„‚) * ↑z + ↑(p 1))) + = norm_sq ∘ f ∘ (Ξ» p : fin 2 β†’ β„€, (coe : β„€ β†’ ℝ) ∘ p), + { ext1, + rw f_def, + dsimp only [function.comp], + rw [of_real_int_cast, of_real_int_cast], }, + rw this, + have hf : f.ker = βŠ₯, + { let g : β„‚ β†’β‚—[ℝ] (fin 2 β†’ ℝ) := + linear_map.pi ![im_lm, im_lm.comp ((z:β„‚) β€’ (conj_ae : β„‚ β†’β‚—[ℝ] β„‚))], + suffices : ((z:β„‚).im⁻¹ β€’ g).comp f = linear_map.id, + { exact linear_map.ker_eq_bot_of_inverse this }, + apply linear_map.ext, + intros c, + have hz : (z:β„‚).im β‰  0 := z.2.ne', + rw [linear_map.comp_apply, linear_map.smul_apply, linear_map.id_apply], + ext i, + dsimp only [g, pi.smul_apply, linear_map.pi_apply, smul_eq_mul], + fin_cases i, + { show ((z : β„‚).im)⁻¹ * (f c).im = c 0, + rw [f_def, add_im, of_real_mul_im, of_real_im, add_zero, mul_left_comm, + inv_mul_cancel hz, mul_one], }, + { show ((z : β„‚).im)⁻¹ * ((z : β„‚) * conj (f c)).im = c 1, + rw [f_def, ring_equiv.map_add, ring_equiv.map_mul, mul_add, mul_left_comm, mul_conj, + conj_of_real, conj_of_real, ← of_real_mul, add_im, of_real_im, zero_add, + inv_mul_eq_iff_eq_mulβ‚€ hz], + simp only [of_real_im, of_real_re, mul_im, zero_add, mul_zero] } }, + have h₁ := (linear_equiv.closed_embedding_of_injective hf).tendsto_cocompact, + have hβ‚‚ : tendsto (Ξ» p : fin 2 β†’ β„€, (coe : β„€ β†’ ℝ) ∘ p) cofinite (cocompact _), + { convert tendsto.pi_map_Coprod (Ξ» i, int.tendsto_coe_cofinite), + { rw Coprod_cofinite }, + { rw Coprod_cocompact } }, + exact tendsto_norm_sq_cocompact_at_top.comp (h₁.comp hβ‚‚) +end + + +/-- Given `coprime_pair` `p=(c,d)`, the matrix `[[a,b],[*,*]]` is sent to `a*c+b*d`. + This is the linear map version of this operation. +-/ +def lc_row0 (p : fin 2 β†’ β„€) : (matrix (fin 2) (fin 2) ℝ) β†’β‚—[ℝ] ℝ := +((p 0:ℝ) β€’ linear_map.proj 0 + (p 1:ℝ) β€’ linear_map.proj 1 : (fin 2 β†’ ℝ) β†’β‚—[ℝ] ℝ).comp + (linear_map.proj 0) + +@[simp] lemma lc_row0_apply (p : fin 2 β†’ β„€) (g : matrix (fin 2) (fin 2) ℝ) : + lc_row0 p g = p 0 * g 0 0 + p 1 * g 0 1 := +rfl + +lemma lc_row0_apply' (a b : ℝ) (c d : β„€) (v : fin 2 β†’ ℝ) : + lc_row0 ![c, d] ![![a, b], v] = c * a + d * b := +by simp + +/-- Linear map sending the matrix [a, b; c, d] to the matrix [acβ‚€ + bdβ‚€, - adβ‚€ + bcβ‚€; c, d], for +some fixed `(cβ‚€, dβ‚€)`. -/ +@[simps] def lc_row0_extend {cd : fin 2 β†’ β„€} (hcd : is_coprime (cd 0) (cd 1)) : + (matrix (fin 2) (fin 2) ℝ) ≃ₗ[ℝ] matrix (fin 2) (fin 2) ℝ := +linear_equiv.Pi_congr_right +![begin + refine linear_map.general_linear_group.general_linear_equiv ℝ (fin 2 β†’ ℝ) + (general_linear_group.to_linear (plane_conformal_matrix (cd 0 : ℝ) (cd 1 : ℝ) _)), + norm_cast, + exact hcd.sq_add_sq_ne_zero + end, + (linear_equiv.refl _ _)] + +/-- The map `lc_row0` is proper, that is, preimages of cocompact sets are finite in +`[[* , *], [c, d]]`.-/ +theorem tendsto_lc_row0 {cd : fin 2 β†’ β„€} (hcd : is_coprime (cd 0) (cd 1)) : + tendsto (Ξ» g : {g : SL(2, β„€) // g 1 = cd}, lc_row0 cd ↑(↑g : SL(2, ℝ))) cofinite (cocompact ℝ) := +begin + let mB : ℝ β†’ (matrix (fin 2) (fin 2) ℝ) := Ξ» t, ![![t, (-(1:β„€):ℝ)], coe ∘ cd], + have hmB : continuous mB, + { refine continuous_pi (Ξ» i, _), + fin_cases i, + { refine continuous_pi (Ξ» j, _), + fin_cases j, + { exact continuous_id }, + { exact @continuous_const _ _ _ _ (-(1:β„€):ℝ) } }, + exact @continuous_const _ _ _ _ (coe ∘ cd) }, + convert filter.tendsto.of_tendsto_comp _ (comap_cocompact hmB), + let f₁ : SL(2, β„€) β†’ matrix (fin 2) (fin 2) ℝ := + Ξ» g, matrix.map (↑g : matrix _ _ β„€) (coe : β„€ β†’ ℝ), + have cocompact_ℝ_to_cofinite_β„€_matrix : + tendsto (Ξ» m : matrix (fin 2) (fin 2) β„€, matrix.map m (coe : β„€ β†’ ℝ)) cofinite (cocompact _), + { convert tendsto.pi_map_Coprod (Ξ» i, tendsto.pi_map_Coprod (Ξ» j, int.tendsto_coe_cofinite)), + { simp [Coprod_cofinite] }, + { simp only [Coprod_cocompact], + refl } }, + have hf₁ : tendsto f₁ cofinite (cocompact _) := + cocompact_ℝ_to_cofinite_β„€_matrix.comp subtype.coe_injective.tendsto_cofinite, + have hfβ‚‚ : closed_embedding (lc_row0_extend hcd) := + (lc_row0_extend hcd).to_continuous_linear_equiv.to_homeomorph.closed_embedding, + convert hfβ‚‚.tendsto_cocompact.comp (hf₁.comp subtype.coe_injective.tendsto_cofinite) using 1, + funext g, + obtain ⟨g, hg⟩ := g, + funext j, + fin_cases j, + { ext i, + fin_cases i, + { simp [mB, f₁, matrix.mul_vec, matrix.dot_product, fin.sum_univ_succ] }, + { convert congr_arg (Ξ» n : β„€, (-n:ℝ)) g.det_coe.symm using 1, + simp [f₁, ← hg, matrix.mul_vec, matrix.dot_product, fin.sum_univ_succ, matrix.det_fin_two, + -special_linear_group.det_coe], + ring } }, + { exact congr_arg (Ξ» p, (coe : β„€ β†’ ℝ) ∘ p) hg.symm } +end + +/-- This replaces `(gβ€’z).re = a/c + *` in the standard theory with the following novel identity: + + `g β€’ z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))` + + which does not need to be decomposed depending on whether `c = 0`. -/ +lemma smul_eq_lc_row0_add {p : fin 2 β†’ β„€} (hp : is_coprime (p 0) (p 1)) (z : ℍ) {g : SL(2,β„€)} + (hg : β†‘β‚˜g 1 = p) : + ↑(g β€’ z) = ((lc_row0 p ↑(g : SL(2, ℝ))) : β„‚) / (p 0 ^ 2 + p 1 ^ 2) + + ((p 1 : β„‚) * z - p 0) / ((p 0 ^ 2 + p 1 ^ 2) * (p 0 * z + p 1)) := +begin + have nonZ1 : (p 0 : β„‚) ^ 2 + (p 1) ^ 2 β‰  0 := by exact_mod_cast hp.sq_add_sq_ne_zero, + have : (coe : β„€ β†’ ℝ) ∘ p β‰  0 := Ξ» h, hp.ne_zero ((@int.cast_injective ℝ _ _ _).comp_left h), + have nonZ2 : (p 0 : β„‚) * z + p 1 β‰  0 := by simpa using linear_ne_zero _ z this, + field_simp [nonZ1, nonZ2, denom_ne_zero, -upper_half_plane.denom, -denom_apply], + rw (by simp : (p 1 : β„‚) * z - p 0 = ((p 1) * z - p 0) * ↑(det (↑g : matrix (fin 2) (fin 2) β„€))), + rw [←hg, det_fin_two], + simp only [int.coe_cast_ring_hom, coe_matrix_coe, coe_fn_eq_coe, + int.cast_mul, of_real_int_cast, map_apply, denom, int.cast_sub], + ring, +end + +lemma tendsto_abs_re_smul (z:ℍ) {p : fin 2 β†’ β„€} (hp : is_coprime (p 0) (p 1)) : + tendsto (Ξ» g : {g : SL(2, β„€) // g 1 = p}, |((g : SL(2, β„€)) β€’ z).re|) + cofinite at_top := +begin + suffices : tendsto (Ξ» g : (Ξ» g : SL(2, β„€), g 1) ⁻¹' {p}, (((g : SL(2, β„€)) β€’ z).re)) + cofinite (cocompact ℝ), + { exact tendsto_norm_cocompact_at_top.comp this }, + have : ((p 0 : ℝ) ^ 2 + p 1 ^ 2)⁻¹ β‰  0, + { apply inv_ne_zero, + exact_mod_cast hp.sq_add_sq_ne_zero }, + let f := homeomorph.mul_rightβ‚€ _ this, + let ff := homeomorph.add_right (((p 1:β„‚)* z - p 0) / ((p 0 ^ 2 + p 1 ^ 2) * (p 0 * z + p 1))).re, + convert ((f.trans ff).closed_embedding.tendsto_cocompact).comp (tendsto_lc_row0 hp), + ext g, + change ((g : SL(2, β„€)) β€’ z).re = (lc_row0 p ↑(↑g : SL(2, ℝ))) / (p 0 ^ 2 + p 1 ^ 2) + + (((p 1:β„‚ )* z - p 0) / ((p 0 ^ 2 + p 1 ^ 2) * (p 0 * z + p 1))).re, + exact_mod_cast (congr_arg complex.re (smul_eq_lc_row0_add hp z g.2)) +end + +end tendsto_lemmas + +section fundamental_domain + +local attribute [simp] coe_smul re_smul + +/-- For `z : ℍ`, there is a `g : SL(2,β„€)` maximizing `(gβ€’z).im` -/ +lemma exists_max_im (z : ℍ) : + βˆƒ g : SL(2, β„€), βˆ€ g' : SL(2, β„€), (g' β€’ z).im ≀ (g β€’ z).im := +begin + classical, + let s : set (fin 2 β†’ β„€) := {cd | is_coprime (cd 0) (cd 1)}, + have hs : s.nonempty := ⟨![1, 1], is_coprime_one_left⟩, + obtain ⟨p, hp_coprime, hp⟩ := + filter.tendsto.exists_within_forall_le hs (tendsto_norm_sq_coprime_pair z), + obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime, + refine ⟨g, Ξ» g', _⟩, + rw [im_smul_eq_div_norm_sq, im_smul_eq_div_norm_sq, div_le_div_left], + { simpa [← hg] using hp (g' 1) (bottom_row_coprime g') }, + { exact z.im_pos }, + { exact norm_sq_denom_pos g' z }, + { exact norm_sq_denom_pos g z }, +end + +/-- Given `z : ℍ` and a bottom row `(c,d)`, among the `g : SL(2,β„€)` with this bottom row, minimize + `|(gβ€’z).re|`. -/ +lemma exists_row_one_eq_and_min_re (z:ℍ) {cd : fin 2 β†’ β„€} (hcd : is_coprime (cd 0) (cd 1)) : + βˆƒ g : SL(2,β„€), β†‘β‚˜g 1 = cd ∧ (βˆ€ g' : SL(2,β„€), β†‘β‚˜g 1 = β†‘β‚˜g' 1 β†’ + |(g β€’ z).re| ≀ |(g' β€’ z).re|) := +begin + haveI : nonempty {g : SL(2, β„€) // g 1 = cd} := let ⟨x, hx⟩ := bottom_row_surj hcd in ⟨⟨x, hx.2⟩⟩, + obtain ⟨g, hg⟩ := filter.tendsto.exists_forall_le (tendsto_abs_re_smul z hcd), + refine ⟨g, g.2, _⟩, + { intros g1 hg1, + have : g1 ∈ ((Ξ» g : SL(2, β„€), g 1) ⁻¹' {cd}), + { rw [set.mem_preimage, set.mem_singleton_iff], + exact eq.trans hg1.symm (set.mem_singleton_iff.mp (set.mem_preimage.mp g.2)) }, + 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]⟩ + +/-- The matrix `T' (= 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]⟩ + +/-- 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]⟩ + +/-- The standard (closed) fundamental domain of the action of `SL(2,β„€)` on `ℍ` -/ +def fundamental_domain : set ℍ := +{z | 1 ≀ (complex.norm_sq z) ∧ |z.re| ≀ (1 : ℝ) / 2} + +localized "notation `π’Ÿ` := fundamental_domain" in modular + +/-- If `|z|<1`, then applying `S` strictly decreases `im` -/ +lemma im_lt_im_S_smul {z : ℍ} (h: norm_sq z < 1) : z.im < (S β€’ z).im := +begin + have : z.im < z.im / norm_sq (z:β„‚), + { have imz : 0 < z.im := im_pos z, + apply (lt_div_iff z.norm_sq_pos).mpr, + nlinarith }, + convert this, + simp only [im_smul_eq_div_norm_sq], + field_simp [norm_sq_denom_ne_zero, norm_sq_ne_zero, S] +end + +/-- Any `z : ℍ` can be moved to `π’Ÿ` by an element of `SL(2,β„€)` -/ +lemma exists_smul_mem_fundamental_domain (z : ℍ) : βˆƒ g : SL(2,β„€), g β€’ z ∈ π’Ÿ := +begin + -- obtain a gβ‚€ which maximizes im (g β€’ z), + obtain ⟨gβ‚€, hgβ‚€βŸ© := exists_max_im z, + -- then among those, minimize re + obtain ⟨g, hg, hg'⟩ := exists_row_one_eq_and_min_re z (bottom_row_coprime gβ‚€), + refine ⟨g, _⟩, + -- `g` has same max im property as `gβ‚€` + have hgβ‚€' : βˆ€ (g' : SL(2,β„€)), (g' β€’ z).im ≀ (g β€’ z).im, + { have hg'' : (g β€’ z).im = (gβ‚€ β€’ z).im, + { rw [im_smul_eq_div_norm_sq, im_smul_eq_div_norm_sq, denom_apply, denom_apply, hg] }, + simpa only [hg''] using hgβ‚€ }, + split, + { -- Claim: `1 ≀ ⇑norm_sq ↑(g β€’ z)`. If not, then `Sβ€’gβ€’z` has larger imaginary part + contrapose! hgβ‚€', + refine ⟨S * g, _⟩, + rw mul_action.mul_smul, + exact im_lt_im_S_smul hgβ‚€' }, + { show |(g β€’ z).re| ≀ 1 / 2, -- if not, then either `T` or `T'` decrease |Re|. + rw abs_le, + split, + { contrapose! hg', + refine ⟨T * g, by simp [T, matrix.mul, matrix.dot_product, fin.sum_univ_succ], _⟩, + rw mul_action.mul_smul, + have : |(g β€’ z).re + 1| < |(g β€’ z).re| := + by cases abs_cases ((g β€’ z).re + 1); cases abs_cases (g β€’ z).re; linarith, + convert this, + simp [T] }, + { contrapose! hg', + refine ⟨T' * g, by simp [T', matrix.mul, matrix.dot_product, fin.sum_univ_succ], _⟩, + rw mul_action.mul_smul, + have : |(g β€’ z).re - 1| < |(g β€’ z).re| := + by cases abs_cases ((g β€’ z).re - 1); cases abs_cases (g β€’ z).re; linarith, + convert this, + simp [T', sub_eq_add_neg] } } +end + +end fundamental_domain + +end modular_group diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index b3398c2f48d9c..fe05d9c0f64ce 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -78,6 +78,14 @@ protected def homeomorph.mul_right (a : G) : continuous_inv_fun := continuous_id.mul continuous_const, .. equiv.mul_right a } +@[simp, to_additive] +lemma homeomorph.coe_mul_right (a : G) : ⇑(homeomorph.mul_right a) = Ξ» g, g * a := rfl + +@[to_additive] +lemma homeomorph.mul_right_symm (a : G) : + (homeomorph.mul_right a).symm = homeomorph.mul_right a⁻¹ := +by { ext, refl } + @[to_additive] lemma is_open_map_mul_right (a : G) : is_open_map (Ξ» x, x * a) := (homeomorph.mul_right a).is_open_map diff --git a/src/topology/homeomorph.lean b/src/topology/homeomorph.lean index 51a013dd73f2f..77cdbdcfa19ee 100644 --- a/src/topology/homeomorph.lean +++ b/src/topology/homeomorph.lean @@ -84,6 +84,8 @@ protected def trans (h₁ : Ξ± β‰ƒβ‚œ Ξ²) (hβ‚‚ : Ξ² β‰ƒβ‚œ Ξ³) : Ξ± β‰ƒβ‚œ Ξ³ : continuous_inv_fun := h₁.continuous_inv_fun.comp hβ‚‚.continuous_inv_fun, to_equiv := equiv.trans h₁.to_equiv hβ‚‚.to_equiv } +@[simp] lemma trans_apply (h₁ : Ξ± β‰ƒβ‚œ Ξ²) (hβ‚‚ : Ξ² β‰ƒβ‚œ Ξ³) (a : Ξ±) : h₁.trans hβ‚‚ a = hβ‚‚ (h₁ a) := rfl + @[simp] lemma homeomorph_mk_coe_symm (a : equiv Ξ± Ξ²) (b c) : ((homeomorph.mk a b c).symm : Ξ² β†’ Ξ±) = a.symm := rfl