Macbeath's presentation of the group of a side-paired polygon

Let σ be a side pairing of a convex hyperbolic polygon P, and let Γ ≤ PSL(2, ℝ) contain the side-pairing maps, with locally finite translates γ • P. These translates cover the upper half-plane, which is simply connected, and the polygon is closed and path-connected. Macbeath's theorem for a tile therefore presents Γ by the polygon itself: the generators are the elements γ whose translate γ • P meets P, and the relations are s * t = u whenever P, s • P and u • P have a common point with u = s * t. No angle or cycle condition is used.

When moreover distinct translates of the interior of P are disjoint, the generators are exactly the identity, the side-pairing maps, and the inverse partial cycle products at the finite vertices, and three distinct generating tiles can only meet at a finite vertex, by ConvexPolygon.SidePairing.exists_vertex_of_mem_carrier_of_mem_two_smul_carrier. Reading these generators as words in the side-pairing maps, and these relations as consequences of the side and vertex cycle relations, is how Poincaré's polygon theorem obtains the presentation of Γ from the polygon.

Main results

• ConvexPolygon.SidePairing.macbeathHom_bijective: Γ is presented by the Macbeath generators and relations of the polygon.
• ConvexPolygon.SidePairing.ker_lift_eq_normalClosure_macbeathRels: the same statement as an equality of subgroups of the free group on the generators.

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, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 9.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.macbeathHom_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) : Function.Bijective ⇑(macbeathHom (↥Γ) P.carrier)

Macbeath's presentation of the group of a polygon. If a subgroup Γ contains the side-pairing maps and its translates of the polygon are locally finite, then Γ is presented by the elements γ with γ • P meeting P, subject to the relations s * t = u for every common point of P, s • P and u • P with u = s * t.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ker_lift_eq_normalClosure_macbeathRels {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) : (FreeGroup.lift Subtype.val).ker = Subgroup.normalClosure (macbeathRels (↥Γ) P.carrier)

Macbeath's presentation of the group of a polygon, as a description of the relations: the words in the Macbeath generators of the polygon that evaluate to the identity in Γ form the normal closure of the Macbeath relations.