Compactness from truncated fundamental sets

The compactness argument for a cusp compactification uses a compact part of a fundamental polygon after removing sufficiently high cusp horodiscs. This file isolates that argument: if, at every choice of cusp heights, one compact subset of the upper half-plane meets all remaining orbits, then the compactified quotient is compact. Finiteness of the cusp orbits allows an arbitrary open cover to be reduced to finitely many cusp neighbourhoods and a finite cover of that compact subset.

The hypothesis is the compact truncation property expected of a fundamental polygon. It is independent of the definition of the compactification.

Main result

• Subgroup.CompactifiedQuotient.compactSpace_of_compact_truncations: compactness from a compact truncated fundamental set at every family of cusp heights.

theorem Subgroup.CompactifiedQuotient.compactSpace_of_compact_truncations {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] [Finite Γ.CuspOrbit] (D : Γ.CuspOrbit → Γ.CuspDatum) (hD : ∀ (C : Γ.CuspOrbit), (D C).cuspOrbit = C) (htrunc : ∀ (A : Γ.CuspOrbit → ℝ), ∃ (K : Set UpperHalfPlane), IsCompact K ∧ ∀ (q : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane), q ∈ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) '' K ∨ ∃ (C : Γ.CuspOrbit), q ∈ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) '' TauCeti.Subgroup.CuspDatum.horodisc (D C) (A C)) : CompactSpace Γ.CompactifiedQuotient

If every truncation of the orbit space outside horodiscs has a compact set of representatives in the upper half-plane, then adjoining the finitely many cusp orbits makes the quotient compact. The datum D C may use any scaling at each cusp orbit.