Proper action of PSL(2, ℝ) on the upper half-plane #
The Möbius action of PSL(2, ℝ) on the upper half-plane is continuous, transitive, isometric
for the hyperbolic metric, and proper. Each of these is descended from the corresponding
property of Mathlib's SL(2, ℝ) action using the surjective quotient map
SL(2, ℝ) → PSL(2, ℝ).
The effective PSL(2, ℝ) action on the upper half-plane is jointly continuous.
The effective PSL(2, ℝ) action on the upper half-plane is by hyperbolic isometries.
The effective PSL(2, ℝ) action on the upper half-plane is transitive.
theorem
TauCeti.UpperHalfPlane.isProperMap_psl_smul_I :
IsProperMap fun (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) => g • UpperHalfPlane.I
The orbit map at I for the effective PSL(2, ℝ) action is proper.
The effective PSL(2, ℝ) action on the upper half-plane is proper.