The triangle group of a hyperbolic triangle

Let P be a hyperbolic triangle, with vertices in ℍ ∪ ∂ℍ. The products of the reflections in two of its sides are orientation-preserving isometries, and they generate the subgroup P.triangleGroup of PSL(2, ℝ): the orientation-preserving half of the group generated by the reflections in the sides of P. It is generated by the three vertex transformations P.vertexReflectionComp i, the products of the reflections in the two sides meeting at vertex i, which satisfy v 2 * v 1 * v 0 = 1. At an ideal vertex the vertex transformation is parabolic.

Poincaré's polygon theorem, applied to the double of P, shows that this group is a cofinite Fuchsian group with the expected presentation when the angles of P are π / m for natural numbers m; see TauCeti.Analysis.Complex.Fuchsian.TriangleOrder.Group.

Main declarations

• ConvexPolygon.vertexReflectionComp: the product of the reflections in the two sides at a vertex.
• ConvexPolygon.vertexReflectionComp_two_mul_one_mul_zero: the product relation v 2 * v 1 * v 0 = 1.
• ConvexPolygon.isParabolic_vertexReflectionComp: the transformation at an ideal vertex is parabolic.
• ConvexPolygon.triangleGroup: the group generated by products of reflections in the sides of a triangle.
• ConvexPolygon.triangleGroup_eq_closure_range_vertexReflectionComp: it is generated by the vertex transformations.
• ConvexPolygon.triangleGroup_rotate: relabelling the vertices does not change it.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §10.6 (triangle groups).

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp (P : ConvexPolygon 3) (i : Fin 3) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The transformation at vertex i of a triangle: the product of the reflections in the two sides meeting there, first in side i - 1 and then in side i. It is elliptic at a finite vertex and parabolic at an ideal one.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_def (P : ConvexPolygon 3) (i : Fin 3) : P.vertexReflectionComp i = geodesicReflectionComp (P.sideGeodesic i) (P.sideGeodesic (i - 1))

The vertex transformation, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_zero (P : ConvexPolygon 3) : P.vertexReflectionComp 0 = geodesicReflectionComp (P.sideGeodesic 0) (P.sideGeodesic 2)

The transformation at P 0 is the product of the reflections in sides 2 and 0.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_one (P : ConvexPolygon 3) : P.vertexReflectionComp 1 = geodesicReflectionComp (P.sideGeodesic 1) (P.sideGeodesic 0)

The transformation at P 1 is the product of the reflections in sides 0 and 1.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_two (P : ConvexPolygon 3) : P.vertexReflectionComp 2 = geodesicReflectionComp (P.sideGeodesic 2) (P.sideGeodesic 1)

The transformation at P 2 is the product of the reflections in sides 1 and 2.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_rotate (P : ConvexPolygon 3) (k i : Fin 3) : (P.rotate k).vertexReflectionComp i = P.vertexReflectionComp (i + k)

Relabelling the vertices relabels the vertex transformations.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_two_mul_one_mul_zero (P : ConvexPolygon 3) : P.vertexReflectionComp 2 * P.vertexReflectionComp 1 * P.vertexReflectionComp 0 = 1

The product relation of a triangle group: the middle reflections cancel in v 2 * v 1 * v 0.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_vertexReflectionComp (P : ConvexPolygon 3) {i : Fin 3} {ξ : OnePoint ℝ} (hi : P.vertex i = Sum.inr ξ) : (P.vertexReflectionComp i).IsParabolic

At an ideal vertex, the vertex transformation is parabolic.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroup (P : ConvexPolygon 3) : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)

The triangle group of a triangle: the subgroup of PSL(2, ℝ) generated by the products of the reflections in two of its sides, that is, the orientation-preserving subgroup of the group generated by the reflections in its sides.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroup_def (P : ConvexPolygon 3) : P.triangleGroup = Subgroup.closure (Set.range fun (ij : Fin 3 × Fin 3) => geodesicReflectionComp (P.sideGeodesic ij.1) (P.sideGeodesic ij.2))

The triangle group, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.geodesicReflectionComp_mem_triangleGroup (P : ConvexPolygon 3) (i j : Fin 3) : geodesicReflectionComp (P.sideGeodesic i) (P.sideGeodesic j) ∈ P.triangleGroup

The product of the reflections in two sides lies in the triangle group.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexReflectionComp_mem_triangleGroup (P : ConvexPolygon 3) (i : Fin 3) : P.vertexReflectionComp i ∈ P.triangleGroup

The vertex transformations lie in the triangle group.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroup_eq_closure_range_vertexReflectionComp (P : ConvexPolygon 3) : P.triangleGroup = Subgroup.closure (Set.range P.vertexReflectionComp)

The triangle group is generated by the vertex transformations.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroup_rotate (P : ConvexPolygon 3) (k : Fin 3) : (P.rotate k).triangleGroup = P.triangleGroup

Relabelling the vertices does not change the triangle group.