The presentation complex of a group presentation

For a group presentation ⟨S | R⟩, with generators S and relators R ⊆ FreeGroup S, the presentation complex TauCeti.PresentationComplex R is the 2-dimensional complex with one vertex, one 1-cell for each generator and one 2-cell for each relator. It is the wedge of circles indexed by S, whose fundamental group is the free group on S (TauCeti.WedgeSum.circleFundamentalGroupMulEquiv), with a 2-cell attached along a loop representing each relator (TauCeti.TwoCellAttachment).

The attached cells make the relators trivial in the fundamental group, so sending the generator s to the loop around the s-th circle defines a homomorphism TauCeti.PresentationComplex.fundamentalGroupHom R from the presented group PresentedGroup R to the fundamental group of the presentation complex at its vertex.

Every homomorphism ψ from the presented group to the fundamental group of a pointed space Z is realized by a based map from the presentation complex to Z (TauCeti.PresentationComplex.exists_mapOfEq_comp_fundamentalGroupHom): send the s-th circle to a loop representing ψ s, and extend over the 2-cells, which is possible because the image of each relator is trivial. Applied to the classifying space of the presented group, which is a K(G, 1) whose fundamental group is identified with G, this shows that the homomorphism from the presented group is injective (TauCeti.PresentationComplex.fundamentalGroupHom_injective).

It is also surjective, because attaching 2-cells induces a surjection on fundamental groups (TauCeti.TwoCellAttachment.surjective_map_incl). So the fundamental group of the presentation complex is the presented group (TauCeti.PresentationComplex.fundamentalGroupMulEquiv). With no relators the presentation complex is the wedge of circles, and this is the free group.

The presentation complex is a CW complex (TauCeti.PresentationComplex.instCWComplex), built from the CW structure of the wedge of circles by attaching the 2-cells: its only 0-cell is the vertex, its 1-cells are the circles of the generators (TauCeti.PresentationComplex.cellOneEquiv), its 2-cells are the disks of the relators (TauCeti.PresentationComplex.cellTwoEquiv), and it has no cells of higher dimension.

Main definitions

• TauCeti.PresentationComplex.attachingLoop: a loop in the wedge of circles representing an element of the free group.
• TauCeti.PresentationComplex R: the presentation complex of ⟨S | R⟩.
• TauCeti.PresentationComplex.basepoint: its vertex.
• TauCeti.PresentationComplex.fundamentalGroupHom: the homomorphism from the presented group to the fundamental group of the presentation complex.
• TauCeti.PresentationComplex.fundamentalGroupMulEquiv: the isomorphism π₁(PresentationComplex R) ≃* PresentedGroup R.
• TauCeti.PresentationComplex.instCWComplex: the CW structure on the presentation complex.
• TauCeti.PresentationComplex.cellOneEquiv, TauCeti.PresentationComplex.cellTwoEquiv: its 1-cells are indexed by the generators and its 2-cells by the relators.

Main results

• TauCeti.PresentationComplex.fundamentalGroupHom_of: the generator s goes to the loop around the s-th circle.
• TauCeti.PresentationComplex.exists_mapOfEq_comp_fundamentalGroupHom: every homomorphism from the presented group to a fundamental group is induced by a based map.
• TauCeti.PresentationComplex.fundamentalGroupHom_injective, TauCeti.PresentationComplex.fundamentalGroupHom_surjective: the homomorphism from the presented group to the fundamental group of the presentation complex is injective and surjective.
• TauCeti.PresentationComplex.fundamentalGroupMulEquiv_mapOfEq_expLoop: the isomorphism sends the loop around the s-th circle to the generator s.
• TauCeti.PresentationComplex.fundamentalGroupMulEquiv_map_incl: the inclusion of the wedge of circles induces the quotient map from the free group to the presented group.
• TauCeti.PresentationComplex.skeletonLT_one, TauCeti.PresentationComplex.isEmpty_cell: the 0-skeleton is the vertex, and there are no cells of dimension at least 3.

References

• A. Hatcher, Algebraic Topology, Section 1.2, Proposition 1.26, Corollary 1.28 and the presentation complex X_G described before it, and Section 1.B for maps into a K(G, 1).

noncomputable def TauCeti.PresentationComplex.attachingLoop {S : Type u} (w : FreeGroup S) : Path (WedgeSum.base fun (x : S) => 1) (WedgeSum.base fun (x : S) => 1)

A loop in the wedge of circles indexed by S, at the wedge point, representing the element w of the free group on S under WedgeSum.circleFundamentalGroupMulEquiv.

@[simp]

theorem TauCeti.PresentationComplex.circleFundamentalGroupMulEquiv_attachingLoop {S : Type u} (w : FreeGroup S) : (WedgeSum.circleFundamentalGroupMulEquiv S) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk (attachingLoop w))) = w

The loop attachingLoop w represents w.

@[reducible, inline]

abbrev TauCeti.PresentationComplex {S : Type u} (R : Set (FreeGroup S)) : Type u

The presentation complex of the presentation ⟨S | R⟩: the wedge of circles indexed by the generators S, with a 2-cell attached along the loop attachingLoop r for each relator r ∈ R. It has one vertex, one 1-cell for each generator and one 2-cell for each relator.

@[reducible, inline]

noncomputable abbrev TauCeti.PresentationComplex.incl {S : Type u} (R : Set (FreeGroup S)) : C(WedgeSum fun (x : S) => 1, PresentationComplex R)

The inclusion of the wedge of circles, the 1-skeleton of the presentation complex.

@[reducible, inline]

noncomputable abbrev TauCeti.PresentationComplex.basepoint {S : Type u} (R : Set (FreeGroup S)) : PresentationComplex R

The vertex of the presentation complex, the image of the wedge point.

noncomputable def TauCeti.PresentationComplex.fundamentalGroupHom {S : Type u} (R : Set (FreeGroup S)) : PresentedGroup R →* FundamentalGroup (PresentationComplex R) (basepoint R)

The homomorphism from the presented group PresentedGroup R to the fundamental group of the presentation complex at its vertex, sending the generator s to the loop around the s-th circle. It is well defined because the 2-cells make the relators trivial.

theorem TauCeti.PresentationComplex.fundamentalGroupHom_mk {S : Type u} {R : Set (FreeGroup S)} (w : FreeGroup S) : (fundamentalGroupHom R) ((PresentedGroup.mk R) w) = (FundamentalGroup.map (incl R) (WedgeSum.base fun (x : S) => 1)) ((WedgeSum.circleFundamentalGroupMulEquiv S).symm w)

The homomorphism from the presented group is induced by the inclusion of the wedge of circles, through the identification of its fundamental group with the free group.

theorem TauCeti.PresentationComplex.fundamentalGroupHom_of {S : Type u} {R : Set (FreeGroup S)} (s : S) : (fundamentalGroupHom R) (PresentedGroup.of s) = (FundamentalGroup.mapOfEq ((incl R).comp (WedgeSum.incl (fun (x : S) => 1) s)) ⋯) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk Circle.expLoop))

The generator s goes to the loop around the s-th circle.

theorem TauCeti.PresentationComplex.exists_mapOfEq_comp_fundamentalGroupHom {S : Type u} {R : Set (FreeGroup S)} {Z : Type v} [TopologicalSpace Z] {z : Z} (ψ : PresentedGroup R →* FundamentalGroup Z z) : ∃ (f : C(PresentationComplex R, Z)) (hf : f (basepoint R) = z), (FundamentalGroup.mapOfEq f hf).comp (fundamentalGroupHom R) = ψ

Homomorphisms out of the presented group are induced by based maps. For a pointed space (Z, z), every homomorphism ψ from the presented group to π₁(Z, z) is the map induced on fundamental groups by a based map from the presentation complex to Z, composed with fundamentalGroupHom R. The map sends the s-th circle around a loop representing ψ s, and extends over the 2-cells because ψ kills the relators.

theorem TauCeti.PresentationComplex.fundamentalGroupHom_injective {S : Type u} {R : Set (FreeGroup S)} : Function.Injective ⇑(fundamentalGroupHom R)

The presented group injects into the fundamental group of the presentation complex. The homomorphism fundamentalGroupHom R has a left inverse, induced by a based map from the presentation complex to the classifying space of the presented group, a K(G, 1) whose fundamental group is identified with the presented group by classifyingSpaceFundamentalGroupMulEquiv.

theorem TauCeti.PresentationComplex.fundamentalGroupHom_surjective {S : Type u} {R : Set (FreeGroup S)} : Function.Surjective ⇑(fundamentalGroupHom R)

The homomorphism from the presented group to the fundamental group of the presentation complex is surjective. Every loop at the vertex is homotopic into the wedge of circles (TwoCellAttachment.surjective_map_incl), whose fundamental group is the free group.

noncomputable def TauCeti.PresentationComplex.fundamentalGroupMulEquiv {S : Type u} (R : Set (FreeGroup S)) : FundamentalGroup (PresentationComplex R) (basepoint R) ≃* PresentedGroup R

The fundamental group of the presentation complex is the presented group. The isomorphism π₁(PresentationComplex R) ≃* PresentedGroup R is the inverse of fundamentalGroupHom R, so the loop around the s-th circle goes to the generator s.

@[simp]

theorem TauCeti.PresentationComplex.fundamentalGroupMulEquiv_symm_apply {S : Type u} {R : Set (FreeGroup S)} (g : PresentedGroup R) : (fundamentalGroupMulEquiv R).symm g = (fundamentalGroupHom R) g

@[simp]

theorem TauCeti.PresentationComplex.fundamentalGroupMulEquiv_fundamentalGroupHom {S : Type u} {R : Set (FreeGroup S)} (g : PresentedGroup R) : (fundamentalGroupMulEquiv R) ((fundamentalGroupHom R) g) = g

theorem TauCeti.PresentationComplex.fundamentalGroupMulEquiv_mapOfEq_expLoop {S : Type u} {R : Set (FreeGroup S)} (s : S) : (fundamentalGroupMulEquiv R) ((FundamentalGroup.mapOfEq ((incl R).comp (WedgeSum.incl (fun (x : S) => 1) s)) ⋯) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk Circle.expLoop))) = PresentedGroup.of s

The loop around the s-th circle goes to the generator s.

@[simp]

theorem TauCeti.PresentationComplex.fundamentalGroupMulEquiv_map_incl {S : Type u} {R : Set (FreeGroup S)} (a : FundamentalGroup (WedgeSum fun (x : S) => 1) (WedgeSum.base fun (x : S) => 1)) : (fundamentalGroupMulEquiv R) ((FundamentalGroup.map (incl R) (WedgeSum.base fun (x : S) => 1)) a) = (PresentedGroup.mk R) ((WedgeSum.circleFundamentalGroupMulEquiv S) a)

The inclusion of the wedge of circles induces the quotient map of the free group. Under the identifications of the fundamental group of the wedge of circles with the free group on S and of that of the presentation complex with the presented group, the inclusion of the wedge induces PresentedGroup.mk R.

The CW structure

@[instance_reducible]

noncomputable instance TauCeti.PresentationComplex.instCWComplex {S : Type u} (R : Set (FreeGroup S)) : Topology.CWComplex Set.univ

The CW structure on the presentation complex. It has one 0-cell, the vertex (TauCeti.PresentationComplex.map_zero), one 1-cell for each generator, the circles of the wedge (TauCeti.PresentationComplex.cellOneEquiv), one 2-cell for each relator, attached along the loop attachingLoop r (TauCeti.PresentationComplex.cellTwoEquiv), and no cells of higher dimension (TauCeti.PresentationComplex.isEmpty_cell).

@[instance_reducible]

noncomputable instance TauCeti.PresentationComplex.instUniqueCellUnivOfNatNat {S : Type u} (R : Set (FreeGroup S)) : Unique (Topology.RelCWComplex.cell Set.univ 0)

The presentation complex has a single 0-cell.

@[simp]

theorem TauCeti.PresentationComplex.map_zero {S : Type u} (R : Set (FreeGroup S)) (i : Topology.RelCWComplex.cell Set.univ 0) (y : Fin 0 → ℝ) : ↑(Topology.RelCWComplex.map 0 i) y = basepoint R

The 0-cell of the presentation complex is its vertex.

noncomputable def TauCeti.PresentationComplex.cellOneEquiv {S : Type u} (R : Set (FreeGroup S)) : Topology.RelCWComplex.cell Set.univ 1 ≃ S

The 1-cells of the presentation complex are indexed by the generators.

@[simp]

theorem TauCeti.PresentationComplex.coe_map_cellOneEquiv_symm {S : Type u} (R : Set (FreeGroup S)) (s : S) : ↑(Topology.RelCWComplex.map 1 ((cellOneEquiv R).symm s)) = ⇑(incl R) ∘ ↑(WedgeSum.circleCellMap S s)

The characteristic map of the 1-cell of the generator s wraps the interval once around the s-th circle of the wedge, TauCeti.WedgeSum.circleCellMap s.

noncomputable def TauCeti.PresentationComplex.cellTwoEquiv {S : Type u} (R : Set (FreeGroup S)) : Topology.RelCWComplex.cell Set.univ 2 ≃ ↑R

The 2-cells of the presentation complex are indexed by the relators.

@[simp]

theorem TauCeti.PresentationComplex.map_cellTwoEquiv_symm {S : Type u} (R : Set (FreeGroup S)) (r : ↑R) (y : ↑(Metric.closedBall 0 1)) : ↑(Topology.RelCWComplex.map 2 ((cellTwoEquiv R).symm r)) ↑y = (CategoryTheory.ConcreteCategory.hom (TwoCellAttachment.diskCell (fun (r : ↑R) => attachingLoop ↑r) r)) ((diskHomeomorphClosedBall 2).symm y)

The characteristic map of the 2-cell of the relator r is the square attached along the loop attachingLoop r, read on the disk.

theorem TauCeti.PresentationComplex.isEmpty_cell {S : Type u} (R : Set (FreeGroup S)) {n : ℕ} (hn : 3 ≤ n) : IsEmpty (Topology.RelCWComplex.cell Set.univ n)

The presentation complex has no cells of dimension at least 3.

theorem TauCeti.PresentationComplex.skeletonLT_one {S : Type u} (R : Set (FreeGroup S)) : ↑(Topology.RelCWComplex.skeletonLT Set.univ 1) = {basepoint R}

The 0-skeleton of the presentation complex is its vertex.