Finiteness of elliptic orbits

For a discrete subgroup of PSL(2, ℝ), points with nontrivial stabilizer are locally isolated: proper discontinuity reduces nearby stabilizers to the stabilizer of the centre, and a nonidentity projective Möbius transformation fixes at most one point of the upper half-plane. Their orbits are therefore locally isolated in the coarse quotient. High cusp horodiscs contain no such points, so a compact cusp compactification has only finitely many elliptic orbits.

This finiteness is needed to form the elliptic-order list in an orbifold signature. It applies whenever the compactification is compact, independently of how compactness was established.

References

Svetlana Katok, Fuchsian Groups, §2.4 and Chapter 4.

theorem Subgroup.exists_nhds_inter_ellipticPoints_subset_singleton (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] (z : UpperHalfPlane) : ∃ U ∈ nhds z, U ∩ (↑(TauCeti.freeLocus (↥Γ) UpperHalfPlane))ᶜ ⊆ {z}

Every point has a neighbourhood containing no elliptic point other than itself.

noncomputable def Subgroup.ellipticOrbits (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Set (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)

An elliptic orbit is an orbit containing a point with nontrivial stabilizer.

@[simp]

theorem Subgroup.quotientMk_mem_ellipticOrbits_iff (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) : ⟦z⟧ ∈ Γ.ellipticOrbits ↔ z ∉ TauCeti.freeLocus (↥Γ) UpperHalfPlane

An orbit is elliptic exactly when a representative has nontrivial stabilizer.

theorem Subgroup.finite_ellipticOrbits (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] [CompactSpace Γ.CompactifiedQuotient] : Γ.ellipticOrbits.Finite

The elliptic orbits in the coarse quotient are finite whenever its cusp compactification is compact.