Macbeath's theorem for a closed set with locally finite translates

Macbeath's theorem, TauCeti.macbeathHom_injective, presents a group acting on a simply connected space from an open path-connected set whose translates cover the space. A fundamental polygon or other tile of a tessellation is closed rather than open. This file proves that the presentation read off from the tile itself is already correct: the generators are the elements g with g • P meeting P, and the relations come from triples of translates of P with a common point.

The bridge is a thickening. Let a group act by isometries on a locally path-connected pseudometric space, and let P be closed and connected with locally finite translates. Each point z has a radius r z > 0 such that every translate of P meeting the ball of radius r z about z contains z. The union V of the balls of radius r z / 2 about points of P is an open neighbourhood of P. Its connected component U containing P is open and path-connected. If finitely many translates gᵢ • U share a point x, choose zᵢ ∈ P with x within r zᵢ / 2 of gᵢ • zᵢ, and let z₀ have the largest radius among them. Every gᵢ • zᵢ then lies within r z₀ of g₀ • z₀, so g₀ • z₀ lies in every gᵢ • P. Hence U and P have the same Macbeath generators and the same Macbeath relations, and the two presented groups are canonically isomorphic.

Main results

• TauCeti.exists_isOpen_isPathConnected_superset_of_locallyFinite: a path-connected open thickening U of P such that finitely many translates of U meet only if the corresponding translates of P do.
• TauCeti.macbeathHom_surjective_of_locallyFinite: the Macbeath generators of P generate the group when the translates of P cover a connected space.
• TauCeti.macbeathHom_injective_of_locallyFinite: the Macbeath relations of P are complete when the space is simply connected.
• TauCeti.ker_lift_eq_normalClosure_macbeathRels_of_locallyFinite: the kernel of evaluating words in the Macbeath generators of P is the normal closure of its Macbeath relations.

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 (presentations from locally finite fundamental polygons).

Comparing the Macbeath presentations of two sets

The thickening of a closed set with locally finite translates

theorem TauCeti.exists_isOpen_isPathConnected_superset_of_locallyFinite {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] [IsIsometricSMul G X] {P : Set X} [LocallyPathConnectedSpace X] (hPc : IsClosed P) (hP : IsConnected P) (hlf : LocallyFinite fun (g : G) => g • P) : ∃ (U : Set X), IsOpen U ∧ IsPathConnected U ∧ P ⊆ U ∧ ∀ (s : Finset G), (⋂ g ∈ s, g • U).Nonempty → (⋂ g ∈ s, g • P).Nonempty

The thickening of a tile. Let G act isometrically on a locally path-connected pseudometric space, and let P be closed and connected with locally finite translates. Then P has a path-connected open neighbourhood U such that finitely many translates of U have a common point only if the corresponding translates of P do.

Macbeath's theorem for a closed set

theorem TauCeti.macbeathHom_surjective_of_locallyFinite {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] {P : Set X} [ConnectedSpace X] (hPc : IsClosed P) (hlf : LocallyFinite fun (g : G) => g • P) (hcover : ⋃ (g : G), g • P = Set.univ) : Function.Surjective ⇑(macbeathHom G P)

The Macbeath generators of a tile generate the group. If the translates of a closed set P are locally finite and cover a connected topological space on which G acts continuously, then the elements g with g • P meeting P generate G.

theorem TauCeti.macbeathHom_injective_of_locallyFinite {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] [IsIsometricSMul G X] {P : Set X} [LocallyPathConnectedSpace X] [SimplyConnectedSpace X] (hPc : IsClosed P) (hP : IsConnected P) (hlf : LocallyFinite fun (g : G) => g • P) (hcover : ⋃ (g : G), g • P = Set.univ) : Function.Injective ⇑(macbeathHom G P)

Macbeath's theorem for a tile. If the translates of a closed connected set P are locally finite and cover a simply connected, locally path-connected pseudometric space on which G acts isometrically, then every relation among the Macbeath generators of P is a consequence of the Macbeath relations of P.

theorem TauCeti.ker_lift_eq_normalClosure_macbeathRels_of_locallyFinite {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] [IsIsometricSMul G X] {P : Set X} [LocallyPathConnectedSpace X] [SimplyConnectedSpace X] (hPc : IsClosed P) (hP : IsConnected P) (hlf : LocallyFinite fun (g : G) => g • P) (hcover : ⋃ (g : G), g • P = Set.univ) : (FreeGroup.lift Subtype.val).ker = Subgroup.normalClosure (macbeathRels G P)

Macbeath's theorem for a tile, as a description of the relations: under the hypotheses of TauCeti.macbeathHom_injective_of_locallyFinite, the kernel of the evaluation of words in the Macbeath generators of P is the normal closure of the Macbeath relations of P.