Exact orders of finite vertex-cycle transformations

The derivative of a side-pairing cycle transformation at its finite vertex is exp (i * cycleAngleSum). Thus a cycle with angle sum 2π / t has transformation of exact order t, including t = 1, and a cycle with angle sum less than 2π has a nonidentity transformation. This supplies the finite-cycle relations used in polygon presentations. Neither discreteness nor a fundamental-domain assumption is needed: the angle condition alone determines this order. The converse angle condition for a fundamental polygon requires no-overlap and is proved in TauCeti.Analysis.Complex.UpperHalfPlane.Polygon.SidePairing.Vertex.Stabilizer.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chapter 3.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.smulDeriv_cycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) : (σ.cycleMap j).smulDeriv z = Complex.exp (↑(σ.cycleAngleSum j) * Complex.I)

The derivative of a cycle transformation at a finite vertex is the unit complex number whose counterclockwise angle is the cycle angle sum.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orderOf_cycleMap_of_cycleAngleSum {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {t : ℕ} (hangle : σ.cycleAngleSum j = 2 * Real.pi / ↑t) : orderOf (σ.cycleMap j) = t

If the angle sum at a finite vertex cycle is 2π / t, its cycle transformation has exact order t. In particular, the relation cannot be shortened to a proper divisor of t.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orderOf_cycleMap_mul_cycleAngleSum_of_sum_eq_two_pi {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {M : ℕ} (hjM : (⇑σ.next)^[M] j = j) (hk' : ∑ l ∈ Finset.range M, P.interiorAngle ((⇑σ.next)^[l] j) = 2 * Real.pi) : ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi

If the M-th tile around a finite vertex returns to the vertex after angles summing to 2π, then the order of the cycle transformation times the cycle angle sum is 2π.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_ne_one_of_cycleAngleSum_lt {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} (hj : (P.vertex j).isLeft = true) (hangle : σ.cycleAngleSum j < 2 * Real.pi) : σ.cycleMap j ≠ 1

A finite vertex cycle whose angle sum is less than 2π has a nonidentity cycle transformation: its derivative at the vertex is the rotation by that angle sum, which lies strictly between 0 and 2π.