Macbeath's presentation of a group acting on a simply connected space

Let a group G act by homeomorphisms on a space X, and let U ⊆ X be an open set whose translates cover X. The elements g for which g • U meets U are the Macbeath generators of U. For two such generators s and t, the product s * t is again one whenever the three sets U, s • U and (s * t) • U have a common point, and the Macbeath relations are the words s t (s t)⁻¹ for all such triples.

Macbeath's theorem says that these generators and relations present G as soon as X is simply connected and U is path-connected:

• if X is connected, the Macbeath generators generate G: the translates of U by the generated subgroup and by its complement are disjoint open sets covering X;
• if X is simply connected and U is path-connected, every relation among the generators is a consequence of the Macbeath relations.

For the second statement, let Γ be the presented group. Glue copies {a} × U, for a : Γ, by identifying (a * s, v) with (a, s • v) whenever both points of U are defined. The resulting space maps to X by (a, v) ↦ a • v. Over a translate g • U, it is the disjoint union of the copies indexed by the preimages of g in Γ, so the map is a covering map. The glued space is path-connected because U is path-connected and consecutive copies along a generator overlap. A covering map from a path-connected space onto a simply connected space is injective, and hence so is Γ → G.

The intended application is to a Fuchsian group acting on the upper half-plane, with U a neighbourhood of a fundamental polygon: it turns the tiling by the polygon into a presentation of the group.

Main definitions

• TauCeti.macbeathGenerators G U: the elements g : G with U ∩ g • U nonempty.
• TauCeti.macbeathRels G U: the Macbeath relations, words in the free group on the generators.
• TauCeti.macbeathHom G U: the evaluation homomorphism from the presented group to G.
• TauCeti.macbeathEquiv: Macbeath's theorem, the presentation of G, as an isomorphism.

Main results

• TauCeti.macbeathHom_surjective: the Macbeath generators of an open set whose translates cover a connected space generate the group; TauCeti.closure_macbeathGenerators_eq_top states this as an equality of subgroups.
• TauCeti.macbeathHom_injective: if moreover the space is simply connected and the set is path-connected, the Macbeath relations are a complete set of relations.
• TauCeti.ker_lift_eq_normalClosure_macbeathRels: the same statement as an equality of subgroups of the free group: the kernel of evaluation is the normal closure of the Macbeath relations.

References

• A. M. Macbeath, Groups of homeomorphisms of a simply connected space, Ann. of Math. (2) 79 (1964), 473–488.

def TauCeti.macbeathGenerators (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (U : Set X) : Set G

The Macbeath generators of a set U: the elements g whose translate g • U meets U.

def TauCeti.macbeathRels (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (U : Set X) : Set (FreeGroup ↑(macbeathGenerators G U))

The Macbeath relations of a set U: the words s t u⁻¹ in its Macbeath generators for which u = s * t and the three sets U, s • U and u • U have a common point.

def TauCeti.macbeathHom (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (U : Set X) : PresentedGroup (macbeathRels G U) →* G

The evaluation of the group presented by the Macbeath generators and relations of U, sending each generator to itself.

@[simp]

theorem TauCeti.mem_macbeathGenerators {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {g : G} : g ∈ macbeathGenerators G U ↔ (U ∩ g • U).Nonempty

@[simp]

theorem TauCeti.mem_macbeathRels {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {r : FreeGroup ↑(macbeathGenerators G U)} : r ∈ macbeathRels G U ↔ ∃ (s : ↑(macbeathGenerators G U)) (t : ↑(macbeathGenerators G U)) (u : ↑(macbeathGenerators G U)), ↑u = ↑s * ↑t ∧ (U ∩ ↑s • U ∩ ↑u • U).Nonempty ∧ r = FreeGroup.of s * FreeGroup.of t * (FreeGroup.of u)⁻¹

@[simp]

theorem TauCeti.macbeathHom_of {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (U : Set X) (s : ↑(macbeathGenerators G U)) : (macbeathHom G U) (PresentedGroup.of s) = ↑s

@[simp]

theorem TauCeti.macbeathHom_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (U : Set X) (w : FreeGroup ↑(macbeathGenerators G U)) : (macbeathHom G U) ((PresentedGroup.mk (macbeathRels G U)) w) = (FreeGroup.lift Subtype.val) w

The evaluation of the presented group on the image of a word in the Macbeath generators is the evaluation of the word itself.

theorem TauCeti.range_macbeathHom {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (U : Set X) : (macbeathHom G U).range = Subgroup.closure (macbeathGenerators G U)

The image of the evaluation of the presented group is the subgroup generated by the Macbeath generators.

theorem TauCeti.one_mem_macbeathGenerators {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} (hU : U.Nonempty) : 1 ∈ macbeathGenerators G U

theorem TauCeti.inv_mem_macbeathGenerators {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {g : G} (hg : g ∈ macbeathGenerators G U) : g⁻¹ ∈ macbeathGenerators G U

theorem TauCeti.macbeath_of_mul_of {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {s t u : ↑(macbeathGenerators G U)} (hu : ↑u = ↑s * ↑t) (h : (U ∩ ↑s • U ∩ ↑u • U).Nonempty) : PresentedGroup.of s * PresentedGroup.of t = PresentedGroup.of u

The defining relation of the presented group: s * t = u for Macbeath generators with u = s * t as soon as U, s • U and u • U have a common point.

theorem TauCeti.macbeath_of_eq_one {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {s : ↑(macbeathGenerators G U)} (hs : ↑s = 1) : PresentedGroup.of s = 1

The Macbeath generator 1 is the identity of the presented group.

@[simp]

theorem TauCeti.macbeath_of_inv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} (s : ↑(macbeathGenerators G U)) : PresentedGroup.of ⟨(↑s)⁻¹, ⋯⟩ = (PresentedGroup.of s)⁻¹

The Macbeath generator s⁻¹ is the inverse of the generator s in the presented group.

theorem TauCeti.mem_range_macbeathHom_of_nonempty {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} {h g : G} (hh : h ∈ (macbeathHom G U).range) (hg : (h • U ∩ g • U).Nonempty) : g ∈ (macbeathHom G U).range

If a translate of U by an element of the image of macbeathHom meets the translate by g, then g also lies in that image.

The space glued from copies of U

theorem TauCeti.macbeathHom_surjective {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [ConnectedSpace X] (hUo : IsOpen U) (hcover : ⋃ (g : G), g • U = Set.univ) : Function.Surjective ⇑(macbeathHom G U)

The Macbeath generators generate the group. If the translates of an open set U cover a connected space, then the elements g with g • U meeting U generate G.

theorem TauCeti.closure_macbeathGenerators_eq_top {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [ConnectedSpace X] (hUo : IsOpen U) (hcover : ⋃ (g : G), g • U = Set.univ) : Subgroup.closure (macbeathGenerators G U) = ⊤

The Macbeath generators generate the group, as a statement about subgroups.

theorem TauCeti.macbeathHom_injective {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U) (hcover : ⋃ (g : G), g • U = Set.univ) : Function.Injective ⇑(macbeathHom G U)

The Macbeath relations are complete. If the translates of a path-connected open set U cover a simply connected space, then every relation among the Macbeath generators of U is a consequence of the Macbeath relations.

noncomputable def TauCeti.macbeathEquiv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U) (hcover : ⋃ (g : G), g • U = Set.univ) : PresentedGroup (macbeathRels G U) ≃* G

Macbeath's theorem. If the translates of a path-connected open set U cover a simply connected space X, then G is presented by the Macbeath generators and relations of U.

@[simp]

theorem TauCeti.macbeathEquiv_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U) (hcover : ⋃ (g : G), g • U = Set.univ) (a : PresentedGroup (macbeathRels G U)) : (macbeathEquiv hUo hUc hcover) a = (macbeathHom G U) a

@[simp]

theorem TauCeti.macbeathEquiv_symm_apply_of {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U) (hcover : ⋃ (g : G), g • U = Set.univ) {g : G} (hg : g ∈ macbeathGenerators G U) : (macbeathEquiv hUo hUc hcover).symm g = PresentedGroup.of ⟨g, hg⟩

theorem TauCeti.ker_lift_eq_normalClosure_macbeathRels {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U) (hcover : ⋃ (g : G), g • U = Set.univ) : (FreeGroup.lift Subtype.val).ker = Subgroup.normalClosure (macbeathRels G U)

Macbeath's theorem, as a description of the relations: if the translates of a path-connected open set U cover a simply connected space, then the kernel of the evaluation of words in the Macbeath generators of U is the normal closure of the Macbeath relations.