The cellular classifying space of a presented group

For a group presentation ⟨S | R⟩, the cellular classifying space TauCeti.cellularClassifyingSpace R is obtained from the presentation complex TauCeti.PresentationComplex R by attaching cells of dimension at least 3 to kill all of its higher homotopy groups: it is TauCeti.killHomotopyGroups 2 of the presentation complex, based at its vertex. The presentation complex is Hausdorff, since it is built from a wedge of circles by attaching disks (TauCeti.TwoCellAttachment.instT2Space), and path connected. So the cellular classifying space is a Hausdorff, path-connected K(PresentedGroup R, 1) (TauCeti.isEilenbergMacLaneSpaceOne_cellularClassifyingSpace). Its fundamental group is identified with the presented group (TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv) by the inclusion of the presentation complex: the generator s corresponds to the loop around the s-th circle of the presentation complex.

Every group G has the tautological presentation, whose generators are the elements of G and whose relators are the kernel of the evaluation map FreeGroup G →* G, so every group has a cellular classifying space, with no finiteness, countability or presentation hypothesis. This is the cellular counterpart of Milnor's classifying space TauCeti.classifyingSpace G; the existence theorem, TauCeti.exists_isEilenbergMacLaneSpaceOne_cellularClassifyingSpace, is stated in TauCeti.AlgebraicTopology.ClassifyingSpace.Comparison together with the standing hypotheses of covering-space theory, the second of which is transported from Milnor's model.

Maps out of this model have the expected universal property: every homomorphism from its fundamental group to the fundamental group of a space with vanishing higher homotopy groups is induced by a pointed map (TauCeti.exists_mapOfEq_cellularClassifyingSpace). The map is first constructed on the presentation complex and then extended across the cells that kill the higher homotopy groups.

The cellular classifying space is a CW complex (TauCeti.instCWComplexCellularClassifyingSpace): the presentation complex is one (TauCeti.PresentationComplex.instCWComplex), with no cells of dimension above 2, and the cells killing the higher homotopy groups have dimension at least 3. In particular it has CW type, so the theory of classical CW complexes, such as Whitehead's theorem, applies to it, and, as a Hausdorff CW complex, it is delta-generated and hence locally path-connected (TauCeti.instDeltaGeneratedSpaceOfCWComplexUniv). Its only 0-cell is the base point (TauCeti.skeletonLT_one_cellularClassifyingSpace), so the pointed maps realizing a homomorphism of fundamental groups are unique up to homotopy relative to the base point (TauCeti.homotopicRel_of_mapOfEq_eq_cellularClassifyingSpace). If the presentation complex is already aspherical, as it is for a presentation of a free group without relators, the cells killing the higher homotopy groups change nothing up to homotopy: by Whitehead's theorem the inclusion of the presentation complex is a homotopy equivalence (TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace).

Main definitions

• TauCeti.cellularClassifyingSpace R: the presentation complex of ⟨S | R⟩ with its higher homotopy groups killed.
• TauCeti.cellularClassifyingSpaceBasepoint R: its base point, the vertex of the presentation complex.
• TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv R: the isomorphism of its fundamental group with PresentedGroup R.
• TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace: for an aspherical presentation complex, its inclusion into the cellular classifying space, as a homotopy equivalence.

Main results

• TauCeti.isEilenbergMacLaneSpaceOne_cellularClassifyingSpace: the cellular classifying space of ⟨S | R⟩ is a K(PresentedGroup R, 1).
• TauCeti.exists_mapOfEq_cellularClassifyingSpace: every homomorphism from the fundamental group of the cellular classifying space to that of a space with vanishing higher homotopy groups is induced by a pointed map.
• TauCeti.instCWComplexCellularClassifyingSpace: the cellular classifying space is a CW complex, with a single 0-cell at its base point (TauCeti.skeletonLT_one_cellularClassifyingSpace).
• TauCeti.homotopicRel_of_mapOfEq_eq_cellularClassifyingSpace: pointed maps from the cellular classifying space to a space with vanishing higher homotopy groups that induce the same homomorphism of fundamental groups are homotopic relative to the base point.

References

• A. Hatcher, Algebraic Topology, Section 1.B, the construction of a K(G, 1) from the presentation complex of G in the proof of Theorem 1B.8, Proposition 1B.9 for maps into a K(G, 1), and Example 4.16.

@[reducible, inline]

noncomputable abbrev TauCeti.cellularClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) : TopCat

The cellular classifying space of the presentation ⟨S | R⟩: the presentation complex TauCeti.PresentationComplex R with cells of dimension at least 3 attached to kill all of its higher homotopy groups at its vertex. It is a K(PresentedGroup R, 1) (TauCeti.isEilenbergMacLaneSpaceOne_cellularClassifyingSpace).

It is an abbreviation, so the API of TauCeti.killHomotopyGroups applies to it directly: it is Hausdorff and path connected, contains the presentation complex as a closed subspace, and is a relative CW complex over it.

@[reducible, inline]

noncomputable abbrev TauCeti.cellularClassifyingSpaceBasepoint {S : Type u} (R : Set (FreeGroup S)) : ↑(cellularClassifyingSpace R)

The base point of the cellular classifying space, the vertex of the presentation complex.

noncomputable def TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv {S : Type u} (R : Set (FreeGroup S)) : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* PresentedGroup R

The fundamental group of the cellular classifying space is the presented group. The inclusion of the presentation complex induces an isomorphism on fundamental groups, and the fundamental group of the presentation complex is PresentedGroup R (TauCeti.PresentationComplex.fundamentalGroupMulEquiv).

@[simp]

theorem TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv_symm_apply {S : Type u} (R : Set (FreeGroup S)) (g : PresentedGroup R) : (cellularClassifyingSpaceFundamentalGroupMulEquiv R).symm g = (FundamentalGroup.map (TopCat.Hom.hom (killHomotopyGroupsIncl 2 (↧(PresentationComplex R)) (PresentationComplex.basepoint R))) (PresentationComplex.basepoint R)) ((PresentationComplex.fundamentalGroupHom R) g)

The inverse of cellularClassifyingSpaceFundamentalGroupMulEquiv R is induced by the inclusion of the presentation complex: it sends g to the image of PresentationComplex.fundamentalGroupHom R g, so the generator s goes to the loop around the s-th circle.

@[simp]

theorem TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv_map_killHomotopyGroupsIncl {S : Type u} (R : Set (FreeGroup S)) (x : FundamentalGroup (PresentationComplex R) (PresentationComplex.basepoint R)) : (cellularClassifyingSpaceFundamentalGroupMulEquiv R) ((FundamentalGroup.map (TopCat.Hom.hom (killHomotopyGroupsIncl 2 (↧(PresentationComplex R)) (PresentationComplex.basepoint R))) (PresentationComplex.basepoint R)) x) = (PresentationComplex.fundamentalGroupMulEquiv R) x

cellularClassifyingSpaceFundamentalGroupMulEquiv R sends the image of a loop of the presentation complex under its inclusion to the class of that loop in the presented group.

theorem TauCeti.isEilenbergMacLaneSpaceOne_cellularClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) : IsEilenbergMacLaneSpaceOne (PresentedGroup R) (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)

The cellular classifying space of ⟨S | R⟩ is a K(PresentedGroup R, 1): it is path connected, its higher homotopy groups vanish, and its fundamental group is the presented group.

theorem TauCeti.exists_mapOfEq_cellularClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) {Z : Type u} [TopologicalSpace Z] {z : Z} (hZ : ∀ (k : ℕ), 2 ≤ k → Subsingleton (HomotopyGroup.Pi k Z z)) (fπ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) →* FundamentalGroup Z z) : ∃ (f : C(↑(cellularClassifyingSpace R), Z)) (hf : f (cellularClassifyingSpaceBasepoint R) = z), FundamentalGroup.mapOfEq f hf = fπ

Homomorphisms out of the fundamental group of a cellular classifying space are induced by pointed maps. If the homotopy groups of (Z, z) vanish in dimensions at least two, every homomorphism from the fundamental group of cellularClassifyingSpace R to π₁(Z, z) is induced by a continuous map taking the base point to z.

The result is stated directly for fundamental groups, without choosing an identification of π₁(Z, z) with another group.

The CW structure

@[instance_reducible]

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

The cellular classifying space is a CW complex. Its cells are those of the presentation complex, one 0-cell, one 1-cell for each generator and one 2-cell for each relator, together with the cells of dimension at least 3 attached to kill the higher homotopy groups (TauCeti.killHomotopyGroupsCWComplexCellEquiv).

@[instance_reducible]

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

The cellular classifying space has a single 0-cell, that of the presentation complex: the tower attaches no cells of dimension 0.

@[simp]

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

The 0-cell of the cellular classifying space is its base point.

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

The 0-skeleton of the cellular classifying space is its base point.

theorem TauCeti.homotopicRel_of_mapOfEq_eq_cellularClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) {Z : Type u_1} [TopologicalSpace Z] (hZ : ∀ (z : Z) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Z z)) {f g : C(↑(cellularClassifyingSpace R), Z)} {z : Z} (hf : f (cellularClassifyingSpaceBasepoint R) = z) (hg : g (cellularClassifyingSpaceBasepoint R) = z) (hfg : FundamentalGroup.mapOfEq f hf = FundamentalGroup.mapOfEq g hg) : f.HomotopicRel g {cellularClassifyingSpaceBasepoint R}

Maps out of the cellular classifying space are determined up to pointed homotopy by their effect on π₁. If the homotopy groups of Z vanish in dimensions at least two, at every point, two maps from cellularClassifyingSpace R to Z that send the base point to z and induce the same homomorphism of fundamental groups are homotopic relative to the base point. Together with TauCeti.exists_mapOfEq_cellularClassifyingSpace, pointed maps into Z up to pointed homotopy correspond to homomorphisms of fundamental groups.

noncomputable def TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace {S : Type u} {R : Set (FreeGroup S)} (h : IsAspherical (PresentationComplex R) (basepoint R)) : ContinuousMap.HomotopyEquiv (PresentationComplex R) ↑(cellularClassifyingSpace R)

An aspherical presentation complex is already a classifying space. If the presentation complex of ⟨S | R⟩ is aspherical, its inclusion into the cellular classifying space is a homotopy equivalence (TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace_toFun): the cells of dimension at least 3 attached to kill the higher homotopy groups change nothing up to homotopy.

@[simp]

theorem TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace_toFun {S : Type u} {R : Set (FreeGroup S)} (h : IsAspherical (PresentationComplex R) (basepoint R)) : (homotopyEquivCellularClassifyingSpace h).toFun = TopCat.Hom.hom (killHomotopyGroupsIncl 2 (↧(PresentationComplex R)) (basepoint R))

The homotopy equivalence TauCeti.PresentationComplex.homotopyEquivCellularClassifyingSpace is the inclusion of the presentation complex.