The relator quotient of a side-paired polygon

The side-identification words and finite-vertex cycle words of a side-paired hyperbolic polygon give a group presented by generators indexed by sides. Evaluating the generators in a group containing the side-pairing transformations factors through this presented group. For a locally finite fundamental polygon, this map is an isomorphism onto the group: this is the presentation part of Poincaré's polygon theorem.

An ideal vertex contributes no finite-order relation. At a finite vertex the cycle word is raised to the order of its cycle transformation, so its image is the identity.

Injectivity is deduced from Macbeath's presentation of the group by the translates meeting the polygon, ConvexPolygon.SidePairing.macbeathHom_bijective. Each such translate is the identity, a side neighbour, or an inverse partial cycle tile at a finite vertex, and so has a word in the side generators. Distinct descriptions of one translate give the same element of the relator quotient: two vertices of one translate are the endpoints of a common side, by convexity. Three distinct tiles meet only at a finite vertex, where the Macbeath relation follows from the cycle relation. This gives an inverse of the evaluation map.

Main results

• ConvexPolygon.SidePairing.relatorQuotientTo_surjective: the side-pairing maps generate the group of a locally finite fundamental polygon.
• ConvexPolygon.SidePairing.relatorQuotientTo_injective: the side and finite-vertex cycle relations imply every relation among the side-pairing maps.
• ConvexPolygon.SidePairing.ker_lift_generatorsIn_eq_normalClosure_relators: the same statement as an equality of subgroups of the free group on the sides.

References

• A. M. Macbeath, Groups of homeomorphisms of a simply connected space, Ann. of Math. (2) 79 (1964), 473–488.
• Alan Beardon, The Geometry of Discrete Groups, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chapter 3.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Set (FreeGroup (Fin n))

The side-identification and finite-vertex cycle relators of a side pairing.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_relators_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {w : FreeGroup (Fin n)} : w ∈ σ.relators ↔ (∃ (i : Fin n), σ.sideRelator i = w) ∨ ∃ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z ∧ w = σ.cycleWord j ^ orderOf (σ.cycleMap j)

A word is a relator exactly when it is a side-identification word or a finite-vertex cycle power.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.sideRelator_mem_relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.sideRelator i ∈ σ.relators

A side-identification word belongs to the relator set.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleWord_pow_mem_relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hj : P.vertex j = Sum.inl z) : σ.cycleWord j ^ orderOf (σ.cycleMap j) ∈ σ.relators

The order relation of a finite vertex belongs to the relator set.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairingHom_eq_one_of_mem_relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {w : FreeGroup (Fin n)} (hw : w ∈ σ.relators) : σ.pairingHom w = 1

Every displayed relator evaluates to the identity in the projective group.

@[reducible, inline]

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

The quotient of the free side group by the side and finite-vertex cycle relations.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotient_sideRelator {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : (PresentedGroup.mk σ.relators) (σ.sideRelator i) = 1

Every side-identification word is trivial in the relator quotient.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotient_cycleWord_pow {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hj : P.vertex j = Sum.inl z) : (PresentedGroup.mk σ.relators) (σ.cycleWord j) ^ orderOf (σ.cycleMap j) = 1

A finite-vertex cycle word has order dividing that of its cycle transformation in the relator quotient.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.generatorsIn {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (i : Fin n) : ↥Γ

Evaluation of the side generators as elements of a subgroup containing all the pairing transformations.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.coe_generatorsIn {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (i : Fin n) : ↑(σ.generatorsIn hmap i) = σ.map i

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.subtype_comp_lift_generatorsIn {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) : Γ.subtype.comp (FreeGroup.lift (σ.generatorsIn hmap)) = σ.pairingHom

Evaluation of side words in a subgroup agrees with evaluation in PSL(2, ℝ).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.lift_generatorsIn_eq_one_of_mem_relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) {w : FreeGroup (Fin n)} (hw : w ∈ σ.relators) : (FreeGroup.lift (σ.generatorsIn hmap)) w = 1

The side-pairing relators hold in every subgroup containing the pairing transformations.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) : σ.RelatorQuotient →* ↥Γ

Evaluate the side-pairing relator quotient in a subgroup containing the pairing maps.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_of {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (i : Fin n) : (σ.relatorQuotientTo hmap) (PresentedGroup.of i) = σ.generatorsIn hmap i

Evaluation of a side generator in the relator quotient is its pairing transformation.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_mk {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (w : FreeGroup (Fin n)) : (σ.relatorQuotientTo hmap) ((PresentedGroup.mk σ.relators) w) = (FreeGroup.lift (σ.generatorsIn hmap)) w

Evaluation after passing to the relator quotient agrees with evaluation of side words.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orderOf_relatorQuotient_cycleWord {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hj : P.vertex j = Sum.inl z) : orderOf ((PresentedGroup.mk σ.relators) (σ.cycleWord j)) = orderOf (σ.cycleMap j)

The cycle word at a finite vertex has exactly the same order in the relator quotient as its transformation. Relations at other sides and vertices cannot shorten this order.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_surjective {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Function.Surjective ⇑(σ.relatorQuotientTo hmap)

The relator quotient maps onto the group of a locally finite fundamental polygon.

Injectivity of the evaluation

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotient_partialCycleWord_eq_one {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hj : P.vertex j = Sum.inl z) {d : ℕ} (hd : σ.partialCycleMap j d = 1) : (PresentedGroup.mk σ.relators) (σ.partialCycleWord j d) = 1

If d steps along the cycle of a finite vertex compose to the identity, then the corresponding partial cycle word is trivial in the relator quotient.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotient_partialCycleWord_eq_of_partialCycleMap_eq {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hj : P.vertex j = Sum.inl z) {a b : ℕ} (hab : σ.partialCycleMap j a = σ.partialCycleMap j b) : (PresentedGroup.mk σ.relators) (σ.partialCycleWord j a) = (PresentedGroup.mk σ.relators) (σ.partialCycleWord j b)

Two partial cycle words at a finite vertex with the same transformation are equal in the relator quotient.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_injective {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Function.Injective ⇑(σ.relatorQuotientTo hmap)

Poincaré's presentation theorem. For a locally finite fundamental polygon, every word in the side generators evaluating to the identity is a consequence of the side relations and the finite-vertex cycle relations.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.relatorQuotientTo_bijective {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Function.Bijective ⇑(σ.relatorQuotientTo hmap)

Poincaré's presentation theorem. The group of a locally finite fundamental polygon is presented by the side generators, the side relations, and the finite-vertex cycle relations.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ker_lift_generatorsIn_eq_normalClosure_relators {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : (FreeGroup.lift (σ.generatorsIn hmap)).ker = Subgroup.normalClosure σ.relators

Poincaré's presentation theorem, as a description of the relations: the words in the side generators evaluating to the identity in the group of a locally finite fundamental polygon form the normal closure of the side and finite-vertex cycle relators.