The free-locus quotient of a Fuchsian group

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup. Its free locus TauCeti.freeLocus Γ ℍ, the set of points of the upper half-plane with trivial stabilizer, is open and Γ-invariant, and Γ acts on it freely, properly discontinuously and by biholomorphisms. The orbit space of the free locus is therefore a Hausdorff, second countable Riemann surface, whose complex charts are pushed forward along the orbit projection, and the orbit projection is a covering map and a local biholomorphism.

At a point with nontrivial stabilizer, an elliptic point, the orbit projection of the whole upper half-plane is not a covering map; its local model there is the power map u ↦ u ^ m of TauCeti.rootsOfUnityBallQuotientHomeomorph.

Main declarations

• Subgroup.isLocalDiffeomorph_quotientMk_freeLocus: the orbit projection of the free locus is a local biholomorphism.

References

• Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter III §3.

theorem Subgroup.isLocalDiffeomorph_quotientMk_freeLocus (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥Γ] : IsLocalDiffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (↑⊤) (Quotient.mk (MulAction.orbitRel ↥Γ ↥(TauCeti.freeLocus (↥Γ) UpperHalfPlane)))

The orbit projection of the free locus of a discrete subgroup of PSL(2, ℝ) is a local biholomorphism onto the free-locus quotient Riemann surface.