The elliptic disc of a point of the upper half-plane #
Let Γ ≤ PSL(2, ℝ) be a subgroup and z a point of the upper half-plane. The stabilizer of z
in Γ acts by hyperbolic isometries fixing z, so it preserves every hyperbolic disc
Subgroup.stabilizerBall Γ z ε about z. If the action of Γ is properly discontinuous — in
particular if Γ is discrete — then for small ε no other element of Γ moves that disc to meet
itself (TauCeti.exists_ball_disjoint_smul_of_notMem_stabilizer). This separation result is the
key input identifying a neighbourhood in the full orbit space with the quotient of the disc by
the finite group MulAction.stabilizer Γ z.
That orbit space is computed here. In the disc coordinate centred at z the stabilizer acts by
the group of m-th roots of unity, m its order
(Subgroup.stabilizerRotationEquiv, Subgroup.discCoordinate_smul_eq_rotation_smul), and the
disc of hyperbolic radius ε becomes the Euclidean disc of radius tanh (ε / 2)
(UpperHalfPlane.image_discCoordinate_ball). The orbit map of a rotation group of order m on a
disc is u ↦ u ^ m (TauCeti.rootsOfUnityBallQuotientHomeomorph), so the orbit space is again a
disc, with coordinate (disc coordinate) ^ m. This power-map model is intended for the later
construction of a smooth chart on the full quotient and the proof that its quotient map has
multiplicity m; those conclusions are not established in this file.
Main declarations #
Subgroup.stabilizerBall: the hyperbolic disc aboutz, as a set invariant under the stabilizer ofz.Subgroup.stabilizerBallHomeomorph: the disc coordinate, as a homeomorphism from that disc onto a Euclidean disc, equivariant forSubgroup.stabilizerRotationEquiv.Subgroup.stabilizerBallQuotientHomeomorph: the orbit space of the invariant disc under the stabilizer is the Euclidean disc of radiustanh (ε / 2) ^ m, with coordinate them-th power of the disc coordinate.Subgroup.stabilizerBallQuotientToQuotient: the induced map from the local orbit space toΓ \ ℍ; for all sufficiently small positive radii it is an open embedding.
References #
- Hershel Farkas and Irwin Kra, Riemann Surfaces, Graduate Texts in Mathematics 71, Springer, second edition, 1992, Chapter I §§4–5.
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.4.
- Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter III §§3–4.
The hyperbolic disc of radius ε about z, as a set invariant under the stabilizer of z
in Γ: that stabilizer acts by hyperbolic isometries fixing z.
Equations
- Γ.stabilizerBall z ε = { carrier := Metric.ball z ε, smul_mem' := ⋯ }
Instances For
The disc coordinate flattens the invariant hyperbolic disc: it is a homeomorphism from
the hyperbolic disc of radius ε about z onto the Euclidean disc of radius tanh (ε / 2)
about 0, carrying the stabilizer action to the rotation action of the m-th roots of unity by
Subgroup.stabilizerBallHomeomorph_smul. Its underlying coordinate and explicit inverse are
holomorphic by UpperHalfPlane.mdifferentiable_discCoordinate and
UpperHalfPlane.analyticOnNhd_discCoordinateHomeomorph_symm.
The stabilizer is assumed finite because the codomain needs it: TauCeti.rootsOfUnityBall m is
defined only for m ≠ 0, and for m = 0 the group rootsOfUnity 0 ℂ is the whole unit group,
which does not preserve a disc. The finiteness-free geometry is
UpperHalfPlane.discCoordinateHomeomorph together with UpperHalfPlane.image_discCoordinate_ball,
of which this is the packaging against the roots-of-unity model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The disc coordinate conjugates the stabilizer action to a rotation action: it is
equivariant along the identification Subgroup.stabilizerRotationEquiv of the stabilizer of z
with the m-th roots of unity.
On the invariant disc, two points lie in the same stabilizer orbit exactly when their disc
coordinates lie in the same orbit of the m-th roots of unity.
The stabilizer quotient coordinate. For 0 ≤ ε, the orbit space of the invariant
hyperbolic disc of radius ε about z under the stabilizer of z, a group of order m, is the
Euclidean disc of radius tanh (ε / 2) ^ m; the identification sends the orbit of τ to the
m-th power of its disc coordinate. A positive radius and a later quotient-neighbourhood
construction are needed to turn this model into a chart on the full Γ-orbit space. The
separation supplied by TauCeti.exists_ball_disjoint_smul_of_notMem_stabilizer is one input to
that later construction.
Equations
Instances For
The map from the orbit space of the disc of radius ε about z under the stabilizer of z
to the orbit space of Γ, sending the orbit of τ to its Γ-orbit.
Equations
Instances For
The map from the local orbit space of a disc to the orbit space of Γ is continuous.
The map from the local orbit space of a disc to the orbit space of Γ is open.
The local orbit space of a small disc is open in Γ \ ℍ. If Γ acts properly
discontinuously, then for every small enough ε > 0 the map from the orbit space of the
hyperbolic disc of radius ε about z under the stabilizer of z to the orbit space of Γ is
an open embedding.