English
If the bottom row has c = 0, then there exists an integer n such that g•z = T^n•z for all z ∈ ℍ.
Русский
Если нижняя строка имеет c = 0, то существует целое n, такое что g•z = T^n•z для всех z ∈ ℍ.
LaTeX
$$$\\forall g \\in SL(2,\\mathbb{Z})\\text{ with } g_{1,0}=0,\\; \\exists n\\in \\mathbb{Z},\\; \\forall z\\in\\mathbb{H},\\; g\\cdot z = T^n\\cdot z.$$$
Lean4
theorem exists_eq_T_zpow_of_c_eq_zero (hc : g 1 0 = 0) : ∃ n : ℤ, ∀ z : ℍ, g • z = T ^ n • z :=
by
have had := g.det_coe
replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; omega
rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
· use g 0 1
suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
ext i j;
fin_cases i <;> fin_cases j <;> simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
· use -(g 0 1)
suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
ext i j;
fin_cases i <;> fin_cases j <;>
simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
-- If `c = 1`, then `g` factorises into a product terms involving only `T` and `S`.
