Side pairings and vertex cycles of a convex hyperbolic polygon

A side pairing of a convex polygon P is an involution pair of its sides together with, for each side i, an element map i of PSL(2, ℝ) carrying side i onto side pair i with the orientation reversed: vertex i ↦ vertex (pair i + 1) and vertex (i + 1) ↦ vertex (pair i), the map of the paired side being the inverse. Following a vertex j through the pairing of the side leaving it, then switching to the other side at the image vertex, is the permutation next : j ↦ pair j + 1 of the vertices. Its orbits are the vertex cycles, and the product of the side-pairing maps along a cycle is the cycle transformation.

Vertices may be finite or ideal, so the paired sides may be segments, rays, or full geodesic lines. No Fuchsian group appears: these are the standalone definitions and their elementary properties.

At a finite vertex cycle, the relation m · sum = 2π between the order of a cycle transformation and the angle sum needs the polygon to be a fundamental domain and is left to Poincaré's polygon theorem.

Main definitions

• ConvexPolygon.SidePairing: a side pairing of a convex polygon.
• ConvexPolygon.SidePairing.next: the successor of a vertex along its cycle, j ↦ pair j + 1.
• ConvexPolygon.SidePairing.cycleLength: the length of the vertex cycle through j.
• ConvexPolygon.SidePairing.partialCycleMap: the product of the first m side-pairing maps along the cycle starting at j.
• ConvexPolygon.SidePairing.cycleMap: the cycle transformation at the vertex j.
• ConvexPolygon.SidePairing.cycle: the vertex cycle through j, as a Finset.
• ConvexPolygon.SidePairing.cycleAngleSum: the sum of the interior angles along a cycle.

Main results

• ConvexPolygon.SidePairing.map_smul_side: the side-pairing map carries side i onto side pair i.
• ConvexPolygon.SidePairing.map_ne_one: a side-pairing map is not the identity.
• ConvexPolygon.SidePairing.cycleMap_smul_vertex: the cycle transformation at j fixes vertex j.
• ConvexPolygon.SidePairing.cycleMap_next: the cycle transformations at the vertices of one cycle are conjugate.
• ConvexPolygon.SidePairing.isElliptic_of_cycleMap_eq: a nonidentity cycle transformation at a vertex in ℍ is elliptic.
• ConvexPolygon.SidePairing.card_cycle: the vertex cycle through j has cycleLength j vertices.
• ConvexPolygon.SidePairing.cycleAngleSum_next, ConvexPolygon.SidePairing.cycleAngleSum_nonneg: the angle sum does not depend on the starting vertex of the cycle, and is nonnegative.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §16.1 (side-pairing transformations), §17.1 (elliptic cycles and elliptic cycle transformations; Remarks 1–2 and the paragraph after Exercise 17.1: an elliptic cycle transformation fixes its vertex, hence is elliptic or the identity), §17.3 (the angle sum along an elliptic cycle).

structure TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing {n : ℕ} [NeZero n] (P : ConvexPolygon n) : Type

A side pairing of the convex polygon P: an involution pair of the sides (side i runs from vertex i to vertex (i + 1)) and, for each side i, an element map i of PSL(2, ℝ) carrying side i onto side pair i with the orientation reversed, the map of the paired side being the inverse. A side may be paired with itself.

• pair : Equiv.Perm (Fin n)

  The side paired with side i.

• pair_pair (i : Fin n) : self.pair (self.pair i) = i

  Pairing is an involution.

• map : Fin n → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

  The transformation carrying side i onto side pair i.

• map_pair (i : Fin n) : self.map (self.pair i) = (self.map i)⁻¹

  The transformation of the paired side is the inverse.

• map_smul_vertex (i : Fin n) : self.map i • P.vertex i = P.vertex (self.pair i + 1)

  The start of side i goes to the end of side pair i.

• map_smul_vertex_add_one (i : Fin n) : self.map i • P.vertex (i + 1) = P.vertex (self.pair i)

  The end of side i goes to the start of side pair i.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ext_iff {n : ℕ} {inst✝ : NeZero n} {P : ConvexPolygon n} {x y : P.SidePairing} : x = y ↔ x.pair = y.pair ∧ x.map = y.map

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ext {n : ℕ} {inst✝ : NeZero n} {P : ConvexPolygon n} {x y : P.SidePairing} (pair : x.pair = y.pair) (map : x.map = y.map) : x = y

The pairing of the sides

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pair_involutive {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Function.Involutive ⇑σ.pair

Pairing is an involution.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pair_symm {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Equiv.symm σ.pair = σ.pair

The inverse of the pairing is the pairing.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_pair_smul_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map (σ.pair i) • P.vertex (σ.pair i + 1) = P.vertex i

The map of the paired side carries the end of side pair i back to the start of side i.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_pair_smul_vertex_add_one {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map (σ.pair i) • P.vertex (σ.pair i) = P.vertex (i + 1)

The map of the paired side carries the start of side pair i back to the end of side i.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_smul_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map i • P.side i = P.side (σ.pair i)

The side-pairing map carries side i onto side pair i.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_ne_one {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map i ≠ 1

A side-pairing map is not the identity.

The vertex successor

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Equiv.Perm (Fin n)

The successor of a vertex along the cycles: the end of the side paired with the side leaving it, j ↦ pair j + 1.

Equations

• σ.next = Equiv.trans σ.pair (Equiv.addRight 1)

@[simp]

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

The successor of j is pair j + 1.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.next_symm_apply {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : (Equiv.symm σ.next) j = σ.pair (j - 1)

The predecessor of j is the pair of the side ending at j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_smul_vertex_eq_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.map j • P.vertex j = P.vertex (σ.next j)

The side-pairing map of the side leaving j carries vertex j to the successor vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_periodicPts_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : j ∈ Function.periodicPts ⇑σ.next

Every vertex is periodic for the successor.

Cycle transformations

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : ℕ → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The product of the first m side-pairing maps along the cycle starting at j: map (next^[m-1] j) * ⋯ * map (next j) * map j.

Equations

• σ.partialCycleMap j 0 = 1
• σ.partialCycleMap j m.succ = σ.map ((⇑σ.next)^[m] j) * σ.partialCycleMap j m

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleMap_zero {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.partialCycleMap j 0 = 1

The empty product of side-pairing maps is the identity.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleMap_succ {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) (m : ℕ) : σ.partialCycleMap j (m + 1) = σ.map ((⇑σ.next)^[m] j) * σ.partialCycleMap j m

The partial products grow by multiplying on the left by the next side-pairing map.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleMap_succ' {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) (m : ℕ) : σ.partialCycleMap j (m + 1) = σ.partialCycleMap (σ.next j) m * σ.map j

The partial products can also be peeled off at the start: the first map applied is the side-pairing map of the side leaving j, followed by the partial product from next j.

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

The partial product of the first m side-pairing maps carries vertex j to the vertex at the m-th successor of j.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleLength {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : ℕ

The length of the vertex cycle through j: the minimal period of j under the successor.

Equations

• σ.cycleLength j = Function.minimalPeriod (⇑σ.next) j

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleLength_def {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleLength j = Function.minimalPeriod (⇑σ.next) j

The cycle length, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleLength_pos {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : 0 < σ.cycleLength j

Cycles are nonempty.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleLength_le {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleLength j ≤ n

A cycle has at most n vertices.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleLength_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleLength (σ.next j) = σ.cycleLength j

The cycle length is constant along a cycle.

@[simp]

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

The cycle length is constant along a cycle, in the simp-normal form of next.

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

Going once around the cycle returns to the starting vertex.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The cycle transformation at the vertex j: the product of the side-pairing maps along the vertex cycle through j, starting with the side leaving j.

Equations

• σ.cycleMap j = σ.partialCycleMap j (σ.cycleLength j)

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_def {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleMap j = σ.partialCycleMap j (σ.cycleLength j)

The cycle transformation, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_smul_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleMap j • P.vertex j = P.vertex j

The cycle transformation at j fixes vertex j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleMap (σ.next j) = σ.map j * σ.cycleMap j * (σ.map j)⁻¹

The cycle transformations along a cycle are conjugate: the one at the successor of j is the conjugate of the one at j by the side-pairing map of the side leaving j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_next_symm {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleMap ((Equiv.symm σ.next) j) = (σ.map ((Equiv.symm σ.next) j))⁻¹ * σ.cycleMap j * σ.map ((Equiv.symm σ.next) j)

The cycle transformation at the predecessor of j is the conjugate of the one at j by the inverse of the side-pairing map of the side leaving the predecessor.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isElliptic_of_cycleMap_eq {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (hj : σ.cycleMap j ≠ 1) {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : ↑g = σ.cycleMap j) : ((Matrix.SpecialLinearGroup.mapGL ℝ) g).IsElliptic

A nonidentity cycle transformation at a vertex in ℍ is elliptic. Ideal vertices are excluded: their cycle transformations instead fix a point of the projective boundary.

Vertex cycles and angle sums

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : Finset (Fin n)

The vertex cycle through j: the orbit of j under the successor.

Equations

• σ.cycle j = {i : Fin n | σ.next.SameCycle j i}

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_cycle_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j i : Fin n) : i ∈ σ.cycle j ↔ ∃ (m : ℕ), (⇑σ.next)^[m] j = i

A vertex i is on the cycle through j if and only if it is an iterated successor of j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.self_mem_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : j ∈ σ.cycle j

A vertex lies on its own cycle.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycle_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycle (σ.next j) = σ.cycle j

The cycle does not depend on the starting vertex.

@[simp]

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

The cycle does not depend on the starting vertex, in the simp-normal form of next.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycle_eq_image {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycle j = Finset.image (fun (m : ℕ) => (⇑σ.next)^[m] j) (Finset.range (σ.cycleLength j))

The cycle through j is enumerated by the first cycleLength j successors of j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.card_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : (σ.cycle j).card = σ.cycleLength j

The number of vertices on the cycle through j is its length.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : ℝ

The angle sum along the vertex cycle through j: the sum of the interior angles of P at the vertices of the cycle.

Equations

• σ.cycleAngleSum j = ∑ i ∈ σ.cycle j, P.interiorAngle i

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum_def {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleAngleSum j = ∑ i ∈ σ.cycle j, P.interiorAngle i

The angle sum along a cycle, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleAngleSum (σ.next j) = σ.cycleAngleSum j

The angle sum does not depend on the starting vertex of the cycle.

@[simp]

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

The angle sum does not depend on the starting vertex, in the simp-normal form of next.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum_nonneg {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : 0 ≤ σ.cycleAngleSum j

The angle sum along a cycle is nonnegative.

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

The angle sum along the cycle of a finite vertex is positive.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleAngleSum_eq_sum_range {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : σ.cycleAngleSum j = ∑ m ∈ Finset.range (σ.cycleLength j), P.interiorAngle ((⇑σ.next)^[m] j)

The angle sum as a sum over the first cycleLength j successors of j.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.cycleAngleSum_pos {n : ℕ} [NeZero n] {P : CompactConvexPolygon n} (σ : P.toConvexPolygon.SidePairing) (j : Fin n) : 0 < σ.cycleAngleSum j

A vertex cycle of a compact convex polygon has positive angle sum.