exists_SL2_smul_eq_of_apply_zero_one_eq_zero

English

If g ∈ SL(2, ℝ) satisfies g(1,0) = 0, then its action on the upper half-plane is an affine map z ↦ u z + v with some u > 0 and v ∈ ℝ.

Русский

Если g ∈ SL(2, ℝ) удовлетворяет g(1,0) = 0, то его действие на верхнюю полуплоскость задаётся афф-The mapping z ↦ u z + v с некоторым u > 0 и v ∈ ℝ.

LaTeX

$$$\exists u>0,\ v \in \mathbb{R}:\ \forall z \in \mathbb{H},\ g\cdot z = u z + v$$$

Lean4

theorem exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : SL(2, ℝ)) (hc : g 1 0 = 0) :
    ∃ (u : { x : ℝ // 0 < x }) (v : ℝ), (g • · : ℍ → ℍ) = (v +ᵥ ·) ∘ (u • ·) :=
  by
  obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc
  refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩
  ext1 ⟨z, hz⟩; ext1
  suffices ↑a * z * a + b * a = b * a + a * a * z by simpa [specialLinearGroup_apply, add_mul]
  ring

Похожие утверждения