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). The acute angles are what makes it strictly convex at P 0 and P 1. Its interior angles there are twice those of P, and at P 2 and its mirror image they equal the angle of P at P 2. Another side of P can be doubled by first relabelling the vertices with ConvexPolygon.rotate.

Its side pairing by products of reflections, used to construct hyperbolic triangle groups, is ConvexPolygon.doubleTriangleSidePairing in TauCeti.Analysis.Complex.UpperHalfPlane.Polygon.SidePairing.DoubleTriangle.

Main declarations #

ConvexPolygon.extGeodesicReflection_sideGeodesic_vertex and ConvexPolygon.extGeodesicReflection_sideGeodesic_vertex_of_add_one_eq: the reflection in a side of a convex polygon fixes the ends of that side.
ConvexPolygon.doubleTriangle: the double of a triangle across side 0.
ConvexPolygon.carrier_doubleTriangle: it is the union of the triangle and its mirror image.
ConvexPolygon.isRight_doubleTriangle_vertex, ConvexPolygon.isLeft_doubleTriangle_vertex: a vertex of the double is ideal or finite as the vertex of P it comes from is.
ConvexPolygon.interiorAngle_doubleTriangle_zero, ConvexPolygon.interiorAngle_doubleTriangle_two: the angles at P 0 and P 1 double.
ConvexPolygon.interiorAngle_doubleTriangle_one, ConvexPolygon.interiorAngle_doubleTriangle_three: the angles at P 2 and at its mirror image are the angle of P at P 2.

References #

Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §10.6 (the fundamental polygon of a triangle group is the union of the triangle and one of its reflections).

source

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.extGeodesicReflection_sideGeodesic_vertex {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) :

extGeodesicReflection (P.sideGeodesic i) (P.vertex i) = P.vertex i

The reflection in the line of a side of a convex polygon fixes the starting vertex of that side.

source

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.extGeodesicReflection_sideGeodesic_vertex_of_add_one_eq {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i j : Fin n} (h : i + 1 = j) :

extGeodesicReflection (P.sideGeodesic i) (P.vertex j) = P.vertex j

The reflection in the line of a side of a convex polygon fixes the final vertex of that side. The index of that vertex is a separate variable, so that simp can use this lemma for explicit indices such as P.vertex 2 and side 1.

source

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

ConvexPolygon 4

The double of a triangle across a side. For a triangle P whose angles at the ends of side 0 are acute, the convex quadrilateral with vertices P 0, the mirror image of P 2 in side 0, P 1 and P 2, in this counterclockwise order. Its carrier is the union of P and its mirror image (carrier_doubleTriangle).

Instances For

source

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangle_vertex {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} :

(P.doubleTriangle h₀ h₁).vertex = ![P.vertex 0, extGeodesicReflection (P.sideGeodesic 0) (P.vertex 2), P.vertex 1, P.vertex 2]

The vertices of the double of a triangle.

source

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isRight_doubleTriangle_vertex {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (j : Fin 4) :

((P.doubleTriangle h₀ h₁).vertex j).isRight = (P.vertex (![0, 2, 1, 2] j)).isRight

A vertex of the double is ideal exactly when the vertex of P it comes from is: the vertices P 0, P 2', P 1, P 2 of the double come from the vertices 0, 2, 1, 2 of P.

source

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isLeft_doubleTriangle_vertex {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} (j : Fin 4) :

((P.doubleTriangle h₀ h₁).vertex j).isLeft = (P.vertex (![0, 2, 1, 2] j)).isLeft

A vertex of the double is finite exactly when the vertex of P it comes from is: the vertices P 0, P 2', P 1, P 2 of the double come from the vertices 0, 2, 1, 2 of P.

source