Reflections in the sides at an ideal vertex

At an ideal vertex ξ of a convex hyperbolic polygon, the geodesic lines of the two sides meeting there both end at ξ, and they are distinct because the polygon is strictly convex. The product of the reflections in two distinct lines with a common ideal endpoint is parabolic (TauCeti.UpperHalfPlane.isParabolic_geodesicReflectionComp_iff): after moving ξ to ∞ the lines are vertical, and the product is a nontrivial translation.

In a hyperbolic triangle group, generated by products of reflections in the sides of a triangle, this identifies the transformations at the ideal vertices of the triangle as parabolic. These are the cycle transformations of the ideal vertices of the doubled triangle, and Poincaré's polygon theorem requires them to be parabolic.

Main result

• ConvexPolygon.isParabolic_geodesicReflectionComp_sideGeodesic: at an ideal vertex, the product of the reflections in the two incident sides is parabolic.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §7.1 (products of two reflections, classified by the relative position of their lines) and §10.6 (triangle groups).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_geodesicReflectionComp_sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : (geodesicReflectionComp (P.sideGeodesic (j - 1)) (P.sideGeodesic j)).IsParabolic

Reflections in the sides at an ideal vertex. At an ideal vertex vertex j of a convex polygon, the product of the reflections in the lines of the two sides meeting there, first in that of side j and then in that of side j - 1, is parabolic.