Fibres over cusps in compactified Fuchsian quotient maps

The fibre of the map of compactified Fuchsian quotients over an adjoined cusp consists exactly of the cusp orbits above it. Together with the boundary-orbit fibre equivalence for finite-index subgroups, this lets orbit and stabilizer calculations on the boundary count these points.

def Subgroup.cuspOrbitFiberEquivCompactifiedFiber {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (C : Γ.CuspOrbit) : { D : Δ.CuspOrbit // cuspOrbitMap h D = C } ≃ { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofCusp C }

The fibre over an adjoined cusp in a compactified quotient map is the fibre of the cusp-orbit map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.cuspOrbitFiberEquivCompactifiedFiber_apply {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (C : Γ.CuspOrbit) (D : { D : Δ.CuspOrbit // cuspOrbitMap h D = C }) : ↑((cuspOrbitFiberEquivCompactifiedFiber h C) D) = CompactifiedQuotient.ofCusp ↑D

The cusp-fibre equivalence inserts a cusp orbit as an adjoined point.