Hyperbolic triangle groups from reflections

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 (see TauCeti.Analysis.Complex.UpperHalfPlane.Polygon.Convex.Triangle.Group).

Suppose that the angles of P are given by a typed triple p, q, r of TriangleOrder parameters: π / m at an elliptic entry of order m, and 0 at a cusp. Such a triangle exists exactly when the triple is hyperbolic (TauCeti.TriangleOrder.isHyperbolic_iff_exists_interiorAngle_eq). Doubling P across a side whose ends have acute angles gives a side-paired quadrilateral satisfying the hypotheses of Poincaré's polygon theorem: its finite vertex cycles have angle sums 2π / m, and the cycle transformations at its ideal vertices are parabolic. Hence:

• P.triangleGroup is a cofinite Fuchsian group, and the double of P is a fundamental domain;
• the abstract triangle group Δ(p, q, r) (TauCeti.TriangleGroup, with a cusp contributing no relation) maps isomorphically onto P.triangleGroup, by sending its generators to the vertex transformations: the presentation is faithful;
• the stabilizer of a finite vertex of P has order the corresponding elliptic order, and P.triangleGroup has one elliptic orbit for each elliptic entry and one cusp for each cusp entry of the triple.

Main declarations

• ConvexPolygon.orderOf_vertexReflectionComp_of_interiorAngle_eq: at a vertex with angle π / m, the vertex transformation has order m.
• ConvexPolygon.isFundamentalDomain_triangleGroup_doubleTriangle: the double of the triangle is a fundamental domain.
• ConvexPolygon.isCofinite_triangleGroup: the triangle group is a cofinite Fuchsian group.
• ConvexPolygon.triangleGroupEquiv: the isomorphism Δ(p, q, r) ≃* P.triangleGroup.
• ConvexPolygon.natCard_stabilizer_triangleGroup, ConvexPolygon.natCard_ellipticOrbits_triangleGroup and ConvexPolygon.natCard_cuspOrbit_triangleGroup: the elliptic orders and the cusp count.
• TriangleOrder.IsHyperbolic.exists_isCofinite_triangleGroup: every hyperbolic typed triple is realised by a cofinite Fuchsian triangle group isomorphic to Δ(p, q, r).

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §10.6 (triangle groups).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §4.3 (Poincaré's theorem and the signature).

The double of a triangle with acute angles at the ends of side 0

theorem TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroup_eq_closure_range_doubleTriangleSidePairing_map {P : ConvexPolygon 3} (h₀ : P.interiorAngle 0 < Real.pi / 2) (h₁ : P.interiorAngle 1 < Real.pi / 2) : P.triangleGroup = Subgroup.closure (Set.range (P.doubleTriangleSidePairing h₀ h₁).map)

The triangle group is generated by the side-pairing maps of the double of the triangle.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_map_mem_triangleGroup {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (i : Fin 4) : (P.doubleTriangleSidePairing h₀ h₁).map i ∈ P.triangleGroup

The side-pairing maps of the double lie in the triangle group.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_vertexReflectionComp_of_interiorAngle_eq {P : ConvexPolygon 3} {i : Fin 3} {m : ℕ} (hi : P.interiorAngle i = Real.pi / ↑m) : orderOf (P.vertexReflectionComp i) = m

The order of a vertex transformation. If P has angle π / m at vertex i, the transformation there has order m. At an ideal vertex the angle is 0, so m = 0: the transformation is parabolic, of infinite order.

Typed angles

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isFundamentalDomain_triangleGroup_doubleTriangle {P : ConvexPolygon 3} {p q r : TriangleOrder} (h₀ : P.interiorAngle 0 < Real.pi / 2) (h₁ : P.interiorAngle 1 < Real.pi / 2) (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : MeasureTheory.IsFundamentalDomain (↥P.triangleGroup) (P.doubleTriangle h₀ h₁).carrier MeasureTheory.volume

The fundamental domain of a triangle group. If the angles of P are given by a typed triple, and those at the ends of side 0 are acute, the double of P is a fundamental domain for the triangle group.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isCofinite_triangleGroup {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : P.triangleGroup.IsCofinite

Hyperbolic triangle groups are cofinite Fuchsian groups. If the angles of P are given by a typed triple of elliptic orders and cusps, the triangle group of P is discrete and has finite covolume.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_vertexReflectionComp {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) (i : Fin 3) : orderOf (P.vertexReflectionComp i) = (![p, q, r] i).order

The orders of the vertex transformations. If the angles of P are given by a typed triple, the transformation at a vertex has the order of the corresponding entry: m at an elliptic entry of order m, and infinite order at a cusp.

The presentation

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.triangleGroupEquiv {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : TriangleGroup p.order q.order r.order ≃* ↥P.triangleGroup

The presentation of a hyperbolic triangle group is faithful. If the angles of P are given by a typed triple p, q, r, the abstract triangle group Δ(p, q, r) = ⟨x, y, z | x ^ p, y ^ q, z ^ r, z * y * x⟩, in which a cusp entry imposes no power relation, is isomorphic to the triangle group of P, by sending x, y, z to the vertex transformations at P 0, P 1, P 2.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.coe_triangleGroupEquiv_x {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : ↑((triangleGroupEquiv hp hq hr) (TriangleGroup.x p.order q.order r.order)) = P.vertexReflectionComp 0

The isomorphism Δ(p, q, r) ≃* P.triangleGroup sends x to the transformation at P 0.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.coe_triangleGroupEquiv_y {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : ↑((triangleGroupEquiv hp hq hr) (TriangleGroup.y p.order q.order r.order)) = P.vertexReflectionComp 1

The isomorphism Δ(p, q, r) ≃* P.triangleGroup sends y to the transformation at P 1.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.coe_triangleGroupEquiv_z {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : ↑((triangleGroupEquiv hp hq hr) (TriangleGroup.z p.order q.order r.order)) = P.vertexReflectionComp 2

The isomorphism Δ(p, q, r) ≃* P.triangleGroup sends z to the transformation at P 2.

Elliptic orders and cusps

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_stabilizer_triangleGroup {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) {i : Fin 3} {z : UpperHalfPlane} (hz : P.vertex i = Sum.inl z) : Nat.card ↥(MulAction.stabilizer (↥P.triangleGroup) z) = (![p, q, r] i).order

The elliptic orders of a triangle group. If the angles of P are given by a typed triple, the stabilizer of a finite vertex of P in its triangle group has the order of the corresponding entry.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_ellipticOrbits_triangleGroup {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : Nat.card ↑P.triangleGroup.ellipticOrbits = {i : Fin (Nat.succ 0).succ.succ | ![p, q, r] i ≠ TriangleOrder.cusp}.card

The number of elliptic orbits of a triangle group. If the angles of P are given by a typed triple, the triangle group of P has one elliptic orbit for each elliptic entry.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_cuspOrbit_triangleGroup {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) : Nat.card P.triangleGroup.CuspOrbit = {i : Fin (Nat.succ 0).succ.succ | ![p, q, r] i = TriangleOrder.cusp}.card

The number of cusps of a triangle group. If the angles of P are given by a typed triple, the triangle group of P has one cusp orbit for each cusp entry.

theorem TauCeti.TriangleOrder.IsHyperbolic.exists_isCofinite_triangleGroup {p q r : TriangleOrder} (h : p.IsHyperbolic q r) : ∃ (P : UpperHalfPlane.ConvexPolygon 3), P.interiorAngle 0 = p.angle ∧ P.interiorAngle 1 = q.angle ∧ P.interiorAngle 2 = r.angle ∧ P.triangleGroup.IsCofinite ∧ Nonempty (TriangleGroup p.order q.order r.order ≃* ↥P.triangleGroup)

Hyperbolic triangle groups. For a hyperbolic typed triple p, q, r of elliptic orders and cusps, some hyperbolic triangle has the corresponding angles, and its triangle group, generated by products of reflections in its sides, is a cofinite Fuchsian group isomorphic to the abstract triangle group Δ(p, q, r).