The compactified quotient of a Fuchsian group: carrier and topology #
Let Γ ≤ PSL(2, ℝ). The compactified quotient Subgroup.CompactifiedQuotient Γ is the
disjoint union of the coarse orbit space Γ \ ℍ and the set Γ.CuspOrbit of cusp orbits of Γ,
one point being adjoined for each cusp orbit. It is the explicit inductive type with constructors
ofQuotient and ofCusp, canonically equivalent to the corresponding sum type.
For a discrete Γ its topology is the usual one: a set is open when its trace on Γ \ ℍ is
open and, for every cusp orbit it contains, it contains the image of a sufficiently high horodisc
at some normalized cusp datum representing that orbit, together with the cusp orbit. The basic
neighbourhoods cuspNhd D A of a cusp orbit are exactly these sets, and every cusp datum
representing the orbit, and every lower bound on the height, gives a neighbourhood basis
(Subgroup.CompactifiedQuotient.nhds_basis_cuspNhd): the topology is independent of the
choice of representative, scaling, and height. This uses that equivalent cusps have proportional
heights (TauCeti.Subgroup.CuspDatum.exists_image_quotientMk_horodisc_eq). Discreteness is
needed for the whole space to be open: it guarantees that every cusp orbit is represented by a
normalized cusp datum (TauCeti.Subgroup.CuspDatum.cuspOrbit_surjective), whereas for a
nondiscrete Γ a cusp may have a noncyclic stabilizer and no such datum.
The coarse quotient embeds as an open subset (isOpenEmbedding_ofQuotient), whose complement is
the closed set of cusp orbits, and is dense. Its preconnectedness therefore extends to the
compactified quotient. The compactified quotient is Hausdorff and second
countable: two cusps are separated by high horodiscs
(TauCeti.Subgroup.CuspDatum.disjoint_image_quotientMk_horodisc_iff), and a point of the orbit
space is separated from a cusp because orbits stay uniformly low near a point
(TauCeti.Subgroup.CuspDatum.exists_isOpen_mem_disjoint_image_quotientMk_horodisc).
Compactness for a cofinite group and the complex structure at the cusps are not part of this
file.
Main declarations #
Subgroup.CompactifiedQuotient: the carrier, with its topology for a discreteΓ.Subgroup.CompactifiedQuotient.equivSum: the identification with the sum type.Subgroup.CompactifiedQuotient.cuspNhd: the basic neighbourhoods of a cusp orbit.Subgroup.CompactifiedQuotient.nhds_basis_cuspNhd: they form a neighbourhood basis, for every cusp datum representing the orbit and every lower bound on the height.Subgroup.CompactifiedQuotient.isOpenEmbedding_ofQuotientandSubgroup.CompactifiedQuotient.dense_range_ofQuotient: the coarse quotient is an open dense subspace.Subgroup.CompactifiedQuotient.instT2SpaceandSubgroup.CompactifiedQuotient.instSecondCountableTopology: the compactified quotient is Hausdorff and second countable.
References #
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Chapter 4.
- Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §§2.4–2.5.
- Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §§18–19.
The compactified quotient of Γ ≤ PSL(2, ℝ): the coarse orbit space Γ \ ℍ with one point
adjoined for each cusp orbit of Γ.
- ofQuotient
{Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
(point : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)
: Γ.CompactifiedQuotient
A point of the coarse orbit space
Γ \ ℍ. - ofCusp
{Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
(cusp : Γ.CuspOrbit)
: Γ.CompactifiedQuotient
The point adjoined for a cusp orbit.
Instances For
The compactified quotient is the sum of the coarse orbit space and the set of cusp orbits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Injectivity of the coarse-quotient inclusion, in the form consumed by the open-embedding API
(compare Sum.inl_injective).
The cusp orbits are exactly the points outside the coarse orbit space.
Cusp neighbourhoods #
The basic neighbourhood of the cusp orbit of the cusp datum D at height A: the cusp orbit
together with the image of the horodisc of height A at D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cusp neighbourhoods shrink as the height grows.
Independence of the cusp datum. Two cusp data representing the same cusp orbit have the same cusp neighbourhoods, up to rescaling the height by a fixed positive factor.
Every cusp neighbourhood at a cusp datum contains a cusp neighbourhood at any other cusp datum representing the same cusp orbit.
Cusp neighbourhoods at two cusp data are disjoint as soon as the horodisc images are and the cusp orbits differ.
The topology #
A set is open when its trace on the coarse orbit space is open and it contains a cusp neighbourhood, at some cusp datum representing it, of every cusp orbit it contains. Discreteness provides a cusp datum for every cusp orbit, so that the whole space is open.
Equations
- One or more equations did not get rendered due to their size.
The coarse orbit space is an open subspace of the compactified quotient.
The cusp orbits form a closed subset of the compactified quotient.
The cusp neighbourhoods form a neighbourhood basis of the cusp orbit, for every cusp datum
representing that orbit and every lower bound A₀ on the height. In particular the topology at a
cusp is independent of the choice of representative, scaling, and height.
Points of the upper half-plane converge to the cusp orbit in the compactified quotient as their height above the cusp, in the scaling coordinate of the datum, tends to infinity.
Density, separation and countability #
The coarse orbit space is dense in the compactified quotient.
The compactified quotient is preconnected: its dense coarse quotient is the continuous image of the connected upper half-plane.
The compactified quotient is Hausdorff.
The compactified quotient is second countable: the coarse orbit space is second countable, there are countably many cusp orbits, and each has the countable neighbourhood basis of cusp neighbourhoods at integer heights.