English
For every z ∈ ℍ, there exists g ∈ SL(2,ℤ) with g•z ∈ 𝒟.
Русский
Пусть z ∈ ℍ; существует g ∈ SL(2,ℤ) такое, что g•z ∈ 𝒟.
LaTeX
$$$\forall z\in \mathbb{H}, \exists g\in SL(2,\mathbb{Z})\; (g\cdot z) \in 𝒟$$$
Lean4
/-- First Fundamental Domain Lemma: Any `z : ℍ` can be moved to `𝒟` by an element of
`SL(2,ℤ)` -/
theorem exists_smul_mem_fd (z : ℍ) : ∃ g : SL(2, ℤ), g • z ∈ 𝒟 := by
-- obtain a g₀ which maximizes im (g • z),
obtain ⟨g₀, hg₀⟩ := exists_max_im z
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 :=
by
have hg'' : (g • z).im = (g₀ • z).im := by
rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq, denom_apply, denom_apply, hg]
simpa only [hg''] using hg₀
constructor
· -- Claim: `1 ≤ ⇑norm_sq ↑(g • z)`. If not, then `S•g•z` has larger imaginary part
contrapose! hg₀'
refine ⟨S * g, ?_⟩
rw [mul_smul]
exact im_lt_im_S_smul hg₀'
· change
|(g • z).re| ≤
1 /
2
-- if not, then either `T` or `T'` decrease |Re|.
rw [abs_le]
constructor
· contrapose! hg'
refine ⟨T * g, (T_mul_apply_one _).symm, ?_⟩
rw [mul_smul, re_T_smul]
cases abs_cases ((g • z).re + 1) <;> cases abs_cases (g • z).re <;> linarith
· contrapose! hg'
refine ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
rw [mul_smul, re_T_inv_smul]
cases abs_cases ((g • z).re - 1) <;> cases abs_cases (g • z).re <;> linarith
