Rotations about I in SL(2, ℝ)

The one-parameter family Matrix.SpecialLinearGroup.rotation θ = !![cos θ, sin θ; -sin θ, cos θ] in SL(2, ℝ) consists of the rotations about I: each fixes I (rotation_smul_I), and rotation (π/2) is, in PSL(2, ℝ), the involution pslS acting as z ↦ -1/z (Matrix.SpecialLinearGroup.pslMk_rotation_pi_div_two). Rotating a point from θ = 0 to θ = π/2 therefore reverses the sign of its real part, so by the intermediate value theorem some rotation moves any point onto the imaginary axis (exists_rotation_smul_re_eq_zero). This is the ingredient that turns transitivity of PSL(2, ℝ) on ℍ into two-point transitivity on geodesic lines (Geodesic.lean).

The stabiliser of I is not identified with the rotation group here, and no rotation angle is computed explicitly.

Main declarations

• TauCeti.UpperHalfPlane.rotation_smul_I — every rotation fixes I.
• TauCeti.UpperHalfPlane.exists_rotation_smul_re_eq_zero — some rotation about I moves any point onto the imaginary axis.

@[simp]

theorem TauCeti.UpperHalfPlane.rotation_smul_I (θ : ℝ) : Matrix.SpecialLinearGroup.rotation θ • UpperHalfPlane.I = UpperHalfPlane.I

The rotations fix I.

theorem TauCeti.UpperHalfPlane.exists_rotation_smul_re_eq_zero (w : UpperHalfPlane) : ∃ θ ∈ Set.Icc 0 (Real.pi / 2), (Matrix.SpecialLinearGroup.rotation θ • w).re = 0

Some rotation about I moves any point onto the imaginary axis.