Ideal vertex cycles of a side-paired hyperbolic polygon

The side-pairing successor preserves whether a vertex lies in the upper half-plane or on its projective boundary. Thus a vertex cycle is entirely finite or entirely ideal. At an ideal vertex, the cycle transformation fixes the boundary point and the cycle angle sum is zero. These statements supply the boundary data for the parabolic cycle condition in a polygon presentation; side-pairing data alone do not imply that an ideal cycle transformation is parabolic.

Main results

• ConvexPolygon.SidePairing.isRight_vertex_of_mem_cycle: all vertices in a cycle have the same type, finite or ideal.
• ConvexPolygon.SidePairing.cycleMap_smul_eq_self_of_vertex_eq_inr: an ideal cycle transformation fixes its boundary vertex.
• ConvexPolygon.SidePairing.cycleAngleSum_eq_zero_of_isRight_vertex: an ideal cycle has zero total angle.

References

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §§17.1–17.2 (elliptic and parabolic cycles). Beardon, The Geometry of Discrete Groups, Chapter 9.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isRight_vertex_pair_add_one {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : (P.vertex (σ.pair j + 1)).isRight = (P.vertex j).isRight

The successor of an ideal vertex is ideal, and the successor of a finite vertex is finite.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isRight_vertex_iterate_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) (m : ℕ) : (P.vertex ((⇑σ.next)^[m] j)).isRight = (P.vertex j).isRight

Following any number of side pairings preserves whether the vertex is ideal.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isRight_vertex_of_mem_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j i : Fin n} (hi : i ∈ σ.cycle j) : (P.vertex i).isRight = (P.vertex j).isRight

Every vertex on a cycle has the same type, finite or ideal, as its starting vertex.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_smul_eq_self_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {c : OnePoint ℝ} (hj : P.vertex j = Sum.inr c) : σ.cycleMap j • c = c

The transformation of a full ideal cycle fixes its projective boundary vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.interiorAngle_eq_zero_of_isRight_vertex_of_mem_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j i : Fin n} (hj : (P.vertex j).isRight = true) (hi : i ∈ σ.cycle j) : P.interiorAngle i = 0

All angles on the cycle of an ideal vertex vanish, since that cycle consists of ideal vertices.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum_eq_zero_of_isRight_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} (hj : (P.vertex j).isRight = true) : σ.cycleAngleSum j = 0

The total angle of an ideal vertex cycle is zero.