Properly discontinuous actions of Fuchsian groups

Every discrete subgroup of PSL(2, ℝ) acts properly discontinuously on the upper half-plane, as a consequence of the proper projective action constructed in TauCeti.Analysis.Complex.UpperHalfPlane.ProperAction.

This supplies the proper-discontinuity input needed to construct Hausdorff orbit quotients and to control stabilizers of Fuchsian groups.

instance TauCeti.instProperlyDiscontinuousSMulSubtypeProjectiveSpecialLinearGroupFinOfNatNatRealMemSubgroupUpperHalfPlaneOfDiscreteTopology_tauCeti (G : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥G] : ProperlyDiscontinuousSMul (↥G) UpperHalfPlane

Every discrete subgroup of PSL(2, ℝ) acts properly discontinuously on the upper half-plane.