The side pairing of the double of a hyperbolic triangle

Let P be a convex hyperbolic triangle, with vertices in ℍ ∪ ∂ℍ, whose interior angles at the two ends P 0, P 1 of side 0 are acute. Reflecting P in the geodesic line of side 0 gives a second triangle, and together they form the convex quadrilateral P.doubleTriangle with vertices P 0, P 2', P 1, P 2, where P 2' is the mirror image of P 2 (ConvexPolygon.carrier_doubleTriangle, in TauCeti.Analysis.Complex.UpperHalfPlane.Polygon.Convex.DoubleTriangle).

Its sides are paired by orientation-preserving products of two reflections in sides of P (ConvexPolygon.doubleTriangleSidePairing): the two sides at P 0 by the product of the reflections in sides 0 and 2, which fixes P 0, and the two sides at P 1 by the product of the reflections in sides 1 and 0, which fixes P 1. In the classical construction of hyperbolic triangle groups, these two products generate the orientation-preserving subgroup of the group generated by the reflections in the sides of a triangle with angles π / p, π / q, π / r, and Poincaré's polygon theorem is applied to this side-paired quadrilateral. Another side of P can be doubled by first relabelling the vertices with ConvexPolygon.rotate.

The vertex cycles of this pairing are {P 0}, {P 1} and {P 2, P 2'}. Their angle sums are twice the angles of P at P 0, P 1 and P 2. The cycle transformation at each vertex of P is the product of the reflections in the two sides of P meeting there; at P 2' it is the conjugate of the inverse of the one at P 2 by the reflection in side 0. So if P has angle π / m at a vertex, the corresponding product of reflections has exact order m: these are the relations of the triangle group.

Main declarations

• ConvexPolygon.doubleTriangleSidePairing: the side pairing of ConvexPolygon.doubleTriangle by products of reflections.
• ConvexPolygon.doubleTriangleSidePairing_cycleLength_zero and its companions: the lengths of the vertex cycles.
• ConvexPolygon.doubleTriangleSidePairing_pair_ne_self: no side of the double is paired with itself, so the type of self-paired sides is empty.
• ConvexPolygon.doubleTriangleSidePairing_sameCycle_iff: two vertices of the double lie on the same cycle exactly when they come from the same vertex of P.
• ConvexPolygon.doubleTriangleSidePairing_cycleMap_ne_one: the cycle transformation at a finite vertex is not the identity.
• ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum and its special cases ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum_zero etc.: the cycle angle sums are twice the angles of P.
• ConvexPolygon.doubleTriangleSidePairing_cycleMap_zero and its companions: the cycle transformations as products of reflections.
• ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap: at a vertex of the double coming from a vertex of P with angle π / m, the cycle transformation has exact order m.
• ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap_mul_cycleAngleSum: if every angle of P is π / m for a natural number m, the double satisfies the angle condition of Poincaré's polygon theorem.
• ConvexPolygon.isParabolic_doubleTriangleSidePairing_cycleMap: the cycle transformations at the ideal vertices of the double are parabolic, the cusp condition of Poincaré's polygon theorem.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §10.6 (triangle groups, generated by products of reflections in the sides of a triangle, with fundamental polygon the union of the triangle and one of its reflections).

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing (P : ConvexPolygon 3) (h₀ : P.interiorAngle 0 < Real.pi / 2) (h₁ : P.interiorAngle 1 < Real.pi / 2) : (P.doubleTriangle h₀ h₁).SidePairing

The side pairing of the double of a triangle. Side i is paired with side 3 - i. The two sides at P 0 are paired by the product of the reflections in sides 0 and 2 of P, which fixes P 0, and the two sides at P 1 by the product of the reflections in sides 1 and 0, which fixes P 1.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_pair (P : ConvexPolygon 3) (h₀ : P.interiorAngle 0 < Real.pi / 2) (h₁ : P.interiorAngle 1 < Real.pi / 2) : (P.doubleTriangleSidePairing h₀ h₁).pair = Fin.revPerm

The side pairing of the double of a triangle pairs side i with side 3 - i.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_map (P : ConvexPolygon 3) (h₀ : P.interiorAngle 0 < Real.pi / 2) (h₁ : P.interiorAngle 1 < Real.pi / 2) : (P.doubleTriangleSidePairing h₀ h₁).map = ![geodesicReflectionComp (P.sideGeodesic 2) (P.sideGeodesic 0), geodesicReflectionComp (P.sideGeodesic 1) (P.sideGeodesic 0), geodesicReflectionComp (P.sideGeodesic 0) (P.sideGeodesic 1), geodesicReflectionComp (P.sideGeodesic 0) (P.sideGeodesic 2)]

The side-pairing maps of the double of a triangle are products of reflections in the sides of the original triangle P.

Vertex cycles

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleLength_zero {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleLength 0 = 1

The vertex P 0 of the double is a cycle of its own.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleLength_two {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleLength 2 = 1

The vertex P 1 of the double is a cycle of its own.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleLength_one {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleLength 1 = 2

The mirror image P 2' of P 2 lies on a cycle of length 2, together with P 2.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleLength_three {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleLength 3 = 2

The vertex P 2 of the double lies on a cycle of length 2, together with P 2'.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum_zero {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum 0 = 2 * P.interiorAngle 0

The angle sum of the cycle at P 0 is twice the angle of P there.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum_two {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum 2 = 2 * P.interiorAngle 1

The angle sum of the cycle at P 1 is twice the angle of P there.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum_one {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum 1 = 2 * P.interiorAngle 2

The angle sum of the cycle through P 2' is twice the angle of P at P 2.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum_three {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum 3 = 2 * P.interiorAngle 2

The angle sum of the cycle through P 2 is twice the angle of P there.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleAngleSum {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (j : Fin 4) : (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum j = 2 * P.interiorAngle (![0, 2, 1, 2] j)

The angle sum of the cycle at a vertex of the double is twice the angle of P at the vertex it comes from.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleMap_zero {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleMap 0 = geodesicReflectionComp (P.sideGeodesic 2) (P.sideGeodesic 0)

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

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleMap_two {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleMap 2 = geodesicReflectionComp (P.sideGeodesic 0) (P.sideGeodesic 1)

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

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleMap_three {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleMap 3 = geodesicReflectionComp (P.sideGeodesic 1) (P.sideGeodesic 2)

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

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleMap_one {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).cycleMap 1 = geodesicReflectionComp (P.sideGeodesic 0) (P.sideGeodesic 2) * geodesicReflectionComp (P.sideGeodesic 1) (P.sideGeodesic 0)

The cycle transformation at P 2' is the product of the reflections in the sides 1 and 2 of P, the inverse of the one at P 2, conjugated by the reflection in side 0.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_pair_ne_self {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (i : Fin 4) : (P.doubleTriangleSidePairing h₀ h₁).pair i ≠ i

No side of the double of a triangle is paired with itself.

instance TauCeti.UpperHalfPlane.ConvexPolygon.instIsEmptySubtypeFinOfNatNatEqCoePermPairDoubleTriangleSidePairing {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : IsEmpty { i : Fin 4 // (P.doubleTriangleSidePairing h₀ h₁).pair i = i }

The double of a triangle has no self-paired side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_next {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} : (P.doubleTriangleSidePairing h₀ h₁).next = Equiv.swap 1 3

The successor along the vertex cycles of the double fixes P 0 and P 1 and exchanges the mirror image P 2' of P 2 with P 2.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_sameCycle_iff {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {j k : Fin 4} : (P.doubleTriangleSidePairing h₀ h₁).next.SameCycle j k ↔ ![0, 2, 1, 2] j = ![0, 2, 1, 2] k

Two vertices of the double lie on the same cycle exactly when they come from the same vertex of P: the vertices P 0, P 2', P 1, P 2 of the double come from the vertices 0, 2, 1, 2 of P.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleSidePairing_cycleMap_ne_one {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {j : Fin 4} (hj : ((P.doubleTriangle h₀ h₁).vertex j).isLeft = true) : (P.doubleTriangleSidePairing h₀ h₁).cycleMap j ≠ 1

At a finite vertex of the double the cycle transformation is not the identity: its cycle angle sum is twice an angle of P, which is strictly between 0 and 2π.

Orders of the cycle transformations

theorem TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {j : Fin 4} {m : ℕ} (hm : m ≠ 0) (hP : P.interiorAngle (![0, 2, 1, 2] j) = Real.pi / ↑m) : orderOf ((P.doubleTriangleSidePairing h₀ h₁).cycleMap j) = m

The relations of the triangle group. If P has angle π / m at the vertex that a vertex of the double comes from, the cycle transformation there has exact order m.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap_mul_cycleAngleSum {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (hP : ∀ (i : Fin 3), ∃ (m : ℕ), P.interiorAngle i = Real.pi / ↑m) (j : Fin 4) (z : UpperHalfPlane) (hz : (P.doubleTriangle h₀ h₁).vertex j = Sum.inl z) : ↑(orderOf ((P.doubleTriangleSidePairing h₀ h₁).cycleMap j)) * (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum j = 2 * Real.pi

The angle condition of Poincaré's theorem. If every angle of P is π / m for a natural number m, then at each finite vertex of the double the order of the cycle transformation times the cycle angle sum is 2π.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_doubleTriangleSidePairing_cycleMap {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (j : Fin 4) (ξ : OnePoint ℝ) (hξ : (P.doubleTriangle h₀ h₁).vertex j = Sum.inr ξ) : ((P.doubleTriangleSidePairing h₀ h₁).cycleMap j).IsParabolic

The cusp condition of Poincaré's theorem. The cycle transformations at the ideal vertices of the double are parabolic.