English
If g ∈ SL(2, ℝ) has g(1,0) ≠ 0, there exist u > 0 and v, w ∈ ℝ such that the Möbius action of g on z is a composition z ↦ w − 1/(u z + v).
Русский
Если g ∈ SL(2, ℝ) имеет g(1,0) ≠ 0, то существует u > 0 и v, w ∈ ℝ такие, что действие g на z представляет собой композицию z ↦ w − 1/(u z + v).
LaTeX
$$$\exists u>0,\ v,w \in \mathbb{R}:\forall z \in \mathbb{H},\ g\cdot z = w - \dfrac{1}{u z + v}$$$
Lean4
theorem exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : SL(2, ℝ)) (hc : g 1 0 ≠ 0) :
∃ (u : { x : ℝ // 0 < x }) (v w : ℝ),
(g • · : ℍ → ℍ) = (w +ᵥ ·) ∘ (ModularGroup.S • · : ℍ → ℍ) ∘ (v +ᵥ · : ℍ → ℍ) ∘ (u • · : ℍ → ℍ) :=
by
have h_denom (z : ℍ) := denom_ne_zero g z
induction g using Matrix.SpecialLinearGroup.fin_two_induction with
| _ a b c d h => ?_
replace hc : c ≠ 0 := by simpa using hc
refine ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, ?_⟩
ext1 ⟨z, hz⟩; ext1
suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
simpa [modular_S_smul, coe_specialLinearGroup_apply]
replace hc : (c : ℂ) ≠ 0 := by norm_cast
replace h_denom : ↑c * z + d ≠ 0 := by simpa using h_denom ⟨z, hz⟩
replace h : (a * d - b * c : ℂ) = (1 : ℂ) := by norm_cast
grind
