Point stabilizers of Fuchsian groups

A discrete subgroup Γ ≤ PSL(2, ℝ) acts properly discontinuously on the upper half-plane, so its point stabilizers are finite, and a finite point stabilizer of a subgroup of PSL(2, ℝ) is cyclic (Subgroup.isCyclic_stabilizer). Hence the point stabilizers of a Fuchsian group are finite cyclic: these are its elliptic stabilizers, generated by a transformation whose derivative at the fixed point is a primitive root of unity of the stabilizer's order (Subgroup.exists_isPrimitiveRoot_stabilizerDeriv).

Main declarations

• Subgroup.instIsCyclicStabilizer: the point stabilizers of a discrete subgroup of PSL(2, ℝ) are cyclic.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 8.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.4.

instance Subgroup.instIsCyclicStabilizer (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] (z : UpperHalfPlane) : IsCyclic ↥(MulAction.stabilizer (↥Γ) z)

The point stabilizers of a Fuchsian group are cyclic: for a discrete subgroup Γ ≤ PSL(2, ℝ), the stabilizer of every point of ℍ is cyclic.