Relations associated to a side pairing

A side pairing of a hyperbolic polygon determines a homomorphism from the free group on its sides to PSL(2, ℝ). Two families of words are intrinsic to the pairing. The side word at i says that the maps attached to i and its paired side are inverse. The cycle word at a vertex is the ordered product of side generators encountered while following the vertex cycle.

This file defines those words and proves their exact evaluations. Thus every side word is a relation, while the t-th power of a cycle word is a relation exactly when the corresponding cycle transformation has order dividing t. These are the algebraic relators used in the presentation part of the Poincaré polygon theorem.

Main definitions

• SidePairing.pairingHom: evaluation of free side words by the side-pairing maps.
• SidePairing.sideRelator: the inverse-pair relation for a side.
• SidePairing.partialCycleWord and SidePairing.cycleWord: the words read along a vertex cycle.

Main results

• SidePairing.cycleWord_next: the cycle words at the vertices of one cycle are conjugate.
• SidePairing.cycleWord_pow_mem_ker_iff: the t-th power of a cycle word is a relation exactly when the order of the cycle transformation divides t.

References

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

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) : FreeGroup (Fin n) →* Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

Evaluate a word in the free group on the sides by the corresponding side-pairing maps.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom_of {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (i : Fin n) : sigma.pairingHom (FreeGroup.of i) = sigma.map i

A free side generator evaluates to its side-pairing map.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.sideRelator {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (i : Fin n) : FreeGroup (Fin n)

The side relation says that the generator of the paired side followed by the original generator is trivial.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.sideRelator_def {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (i : Fin n) : sigma.sideRelator i = FreeGroup.of (sigma.pair i) * FreeGroup.of i

The side relator is the paired-side generator followed by the original generator.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom_sideRelator {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (i : Fin n) : sigma.pairingHom (sigma.sideRelator i) = 1

Every side relator evaluates to the identity.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) : ℕ → FreeGroup (Fin n)

The word in side generators encountered during the first m steps of the vertex cycle starting at j. Its multiplication order matches partialCycleMap.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord_zero {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) : sigma.partialCycleWord j 0 = 1

The empty partial cycle word is the identity.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord_succ {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (m : ℕ) : sigma.partialCycleWord j (m + 1) = FreeGroup.of ((⇑sigma.next)^[m] j) * sigma.partialCycleWord j m

A partial cycle word grows by adjoining the next side generator on the left.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord_succ' {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (m : ℕ) : sigma.partialCycleWord j (m + 1) = sigma.partialCycleWord (sigma.next j) m * FreeGroup.of j

A partial cycle word can instead be read after removing its first side generator.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord_add {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (a b : ℕ) : sigma.partialCycleWord j (a + b) = sigma.partialCycleWord ((⇑sigma.next)^[a] j) b * sigma.partialCycleWord j a

The partial cycle words are multiplicative along the cycle: the first a + b generators from j are the first a generators from j, followed by the first b from next^[a] j.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom_partialCycleWord {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (m : ℕ) : sigma.pairingHom (sigma.partialCycleWord j m) = sigma.partialCycleMap j m

Evaluating a partial cycle word gives the corresponding partial cycle transformation.

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

The cycle word at j, obtained by reading the side generators through one minimal vertex cycle.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleWord_def {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) : sigma.cycleWord j = sigma.partialCycleWord j (sigma.cycleLength j)

The cycle word is the partial cycle word of minimal cycle length.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom_cycleWord {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) : sigma.pairingHom (sigma.cycleWord j) = sigma.cycleMap j

Evaluating the cycle word gives the cycle transformation.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleWord_mul_cycleLength {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (k : ℕ) : sigma.partialCycleWord j (k * sigma.cycleLength j) = sigma.cycleWord j ^ k

Going k times around the cycle through j gives the k-th power of the cycle word.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleWord_next {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) : sigma.cycleWord (sigma.next j) = FreeGroup.of j * sigma.cycleWord j * (FreeGroup.of j)⁻¹

The cycle words along a cycle are conjugate: the one at the successor of j is the conjugate of the one at j by the generator of the side leaving j.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isConj_cycleWord_of_mem_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) {j i : Fin n} (hi : i ∈ sigma.cycle j) : IsConj (sigma.cycleWord j) (sigma.cycleWord i)

Cycle words based at vertices on the same vertex cycle are conjugate in the free side group. In particular, imposing a cycle relation at one vertex imposes it throughout the cycle.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleWord_pow_mem_ker_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (sigma : P.SidePairing) (j : Fin n) (t : ℕ) : sigma.cycleWord j ^ t ∈ sigma.pairingHom.ker ↔ orderOf (sigma.cycleMap j) ∣ t

The t-th power of a cycle word is a relation exactly when the order of the cycle transformation divides t.