The cellular and the simplicial classifying spaces agree

Let ⟨S | R⟩ be a group presentation. The cellular classifying space TauCeti.cellularClassifyingSpace R is a CW complex and a K(PresentedGroup R, 1). Out of it, every isomorphism φ of its fundamental group with the fundamental group of an aspherical space Y of CW type is realized by a homotopy equivalence TauCeti.cellularClassifyingSpaceHomotopyEquiv R hY φ : cellularClassifyingSpace R ≃ₕ Y, whose forward map is pointed: it sends the base point to y and induces exactly φ on fundamental groups. A pointed map realizing φ exists (TauCeti.exists_mapOfEq_cellularClassifyingSpace); it is a weak homotopy equivalence because both spaces are aspherical, hence a homotopy equivalence by Whitehead's theorem. The forward map is determined by φ up to homotopy relative to the base point (TauCeti.homotopicRel_cellularClassifyingSpaceHomotopyEquiv_toFun), since the cellular classifying space has a single 0-cell. The homotopy inverse need not be pointed; it induces φ⁻¹ after a change of base point along a path (TauCeti.exists_path_map_cellularClassifyingSpaceHomotopyEquiv_invFun).

Applied to Milnor's classifying space TauCeti.classifyingSpace G, which is a CW complex and a K(G, 1), this compares the two models of the classifying space of a group: for every isomorphism e : PresentedGroup R ≃* G, TauCeti.cellularHomotopyEquivClassifyingSpace R e is a homotopy equivalence from the cellular to the simplicial model, inducing e under the identifications TauCeti.cellularClassifyingSpaceFundamentalGroupMulEquiv and TauCeti.classifyingSpaceFundamentalGroupMulEquiv of both fundamental groups. Every group has a presentation, for instance the tautological one, so this applies to every group.

Semilocal simple connectivity is a homotopy invariant (ContinuousMap.HomotopyEquiv.semilocallySimplyConnectedSpace), and Milnor's classifying space has it, so the cellular classifying space is semilocally simply connected as well (TauCeti.instSemilocallySimplyConnectedSpaceCellularClassifyingSpace). Being a Hausdorff CW complex, it is also locally path-connected. So the existence theorem for the cellular model, TauCeti.exists_isEilenbergMacLaneSpaceOne_cellularClassifyingSpace, carries the standing hypotheses of covering-space theory exactly as the existence theorem for Milnor's model, TauCeti.exists_isEilenbergMacLaneSpaceOne, does.

Main definitions

• TauCeti.cellularClassifyingSpaceHomotopyEquiv: the homotopy equivalence from the cellular classifying space to an aspherical space of CW type realizing a given isomorphism of fundamental groups by a pointed forward map.
• TauCeti.cellularHomotopyEquivClassifyingSpace: the homotopy equivalence from the cellular classifying space of a presentation of G to Milnor's classifying space of G.

Main results

• TauCeti.mapOfEq_cellularClassifyingSpaceHomotopyEquiv_toFun_apply: the forward map induces φ on fundamental groups.
• TauCeti.homotopicRel_cellularClassifyingSpaceHomotopyEquiv_toFun: every pointed map realizing φ is homotopic to the forward map relative to the base point.
• TauCeti.exists_path_map_cellularClassifyingSpaceHomotopyEquiv_invFun: the homotopy inverse induces φ⁻¹, up to a change of base point.
• TauCeti.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq_cellularHomotopyEquivClassifyingSpace and its counterpart for the inverse: the comparison of the two models induces e and e⁻¹ under the identifications of both fundamental groups with G.
• TauCeti.homotopicRel_cellularHomotopyEquivClassifyingSpace_toFun: the comparison of the two models is determined by e up to homotopy relative to the base point.
• TauCeti.instSemilocallySimplyConnectedSpaceCellularClassifyingSpace: the cellular classifying space is semilocally simply connected.
• TauCeti.exists_isEilenbergMacLaneSpaceOne_cellularClassifyingSpace: every group G has a presentation whose cellular classifying space is a K(G, 1), locally path-connected and semilocally simply connected.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 1.B, Theorem 1B.8 and Proposition 1B.9, and Section 4.1, Theorem 4.5.
• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

noncomputable def TauCeti.cellularClassifyingSpaceHomotopyEquiv {S : Type u} (R : Set (FreeGroup S)) {Y : Type u} [TopologicalSpace Y] [CWType Y] {y : Y} (hY : IsAspherical Y y) (φ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* FundamentalGroup Y y) : ContinuousMap.HomotopyEquiv (↑(cellularClassifyingSpace R)) Y

The cellular classifying space is homotopy equivalent to every aspherical space of CW type with the same fundamental group. For an isomorphism φ from the fundamental group of cellularClassifyingSpace R to π₁(Y, y), this is a homotopy equivalence whose forward map sends the base point to y (TauCeti.cellularClassifyingSpaceHomotopyEquiv_toFun_basepoint) and induces φ on fundamental groups (TauCeti.mapOfEq_cellularClassifyingSpaceHomotopyEquiv_toFun_apply). The forward map is unique up to homotopy relative to the base point (TauCeti.homotopicRel_cellularClassifyingSpaceHomotopyEquiv_toFun).

@[simp]

theorem TauCeti.cellularClassifyingSpaceHomotopyEquiv_toFun_basepoint {S : Type u} (R : Set (FreeGroup S)) {Y : Type u} [TopologicalSpace Y] [CWType Y] {y : Y} (hY : IsAspherical Y y) (φ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* FundamentalGroup Y y) : (cellularClassifyingSpaceHomotopyEquiv R hY φ).toFun (cellularClassifyingSpaceBasepoint R) = y

The forward map of TauCeti.cellularClassifyingSpaceHomotopyEquiv is pointed.

@[simp]

theorem TauCeti.mapOfEq_cellularClassifyingSpaceHomotopyEquiv_toFun_apply {S : Type u} (R : Set (FreeGroup S)) {Y : Type u} [TopologicalSpace Y] [CWType Y] {y : Y} (hY : IsAspherical Y y) (φ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* FundamentalGroup Y y) (a : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)) : (FundamentalGroup.mapOfEq (cellularClassifyingSpaceHomotopyEquiv R hY φ).toFun ⋯) a = φ a

The forward map of TauCeti.cellularClassifyingSpaceHomotopyEquiv induces φ on fundamental groups.

theorem TauCeti.homotopicRel_cellularClassifyingSpaceHomotopyEquiv_toFun {S : Type u} (R : Set (FreeGroup S)) {Y : Type u} [TopologicalSpace Y] [CWType Y] {y : Y} (hY : IsAspherical Y y) (φ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* FundamentalGroup Y y) {f : C(↑(cellularClassifyingSpace R), Y)} (hf : f (cellularClassifyingSpaceBasepoint R) = y) (hfφ : ∀ (a : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)), (FundamentalGroup.mapOfEq f hf) a = φ a) : f.HomotopicRel (cellularClassifyingSpaceHomotopyEquiv R hY φ).toFun {cellularClassifyingSpaceBasepoint R}

The forward map of TauCeti.cellularClassifyingSpaceHomotopyEquiv is determined by φ up to pointed homotopy. Every map from the cellular classifying space to Y that sends the base point to y and induces φ on fundamental groups is homotopic to it relative to the base point.

theorem TauCeti.exists_path_map_cellularClassifyingSpaceHomotopyEquiv_invFun {S : Type u} (R : Set (FreeGroup S)) {Y : Type u} [TopologicalSpace Y] [CWType Y] {y : Y} (hY : IsAspherical Y y) (φ : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R) ≃* FundamentalGroup Y y) : ∃ (γ : Path ((cellularClassifyingSpaceHomotopyEquiv R hY φ).invFun y) (cellularClassifyingSpaceBasepoint R)), ∀ (a : FundamentalGroup Y y), (FundamentalGroup.fundamentalGroupMulEquivOfPath γ) ((FundamentalGroup.map (cellularClassifyingSpaceHomotopyEquiv R hY φ).invFun y) a) = φ.symm a

The homotopy inverse of TauCeti.cellularClassifyingSpaceHomotopyEquiv induces φ⁻¹, up to a change of base point. The inverse need not send y to the base point, but there is a path γ from its value at y to the base point such that the induced map on fundamental groups, followed by basepoint change along γ, is φ⁻¹.

noncomputable def TauCeti.cellularHomotopyEquivClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) {G : Type u} [Group G] (e : PresentedGroup R ≃* G) : ContinuousMap.HomotopyEquiv (↑(cellularClassifyingSpace R)) (classifyingSpace G)

The cellular and the simplicial classifying spaces agree. For a presentation e : PresentedGroup R ≃* G of G, this is a homotopy equivalence from the cellular classifying space cellularClassifyingSpace R to Milnor's classifying space classifyingSpace G. Its forward map is pointed, induces e under the identifications of both fundamental groups (TauCeti.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq_cellularHomotopyEquivClassifyingSpace), and is unique up to pointed homotopy (TauCeti.homotopicRel_cellularHomotopyEquivClassifyingSpace_toFun). Its homotopy inverse induces e⁻¹ up to a change of base point (TauCeti.exists_path_map_cellularHomotopyEquivClassifyingSpace_invFun).

@[simp]

theorem TauCeti.cellularHomotopyEquivClassifyingSpace_toFun_basepoint {S : Type u} (R : Set (FreeGroup S)) {G : Type u} [Group G] (e : PresentedGroup R ≃* G) : (cellularHomotopyEquivClassifyingSpace R e).toFun (cellularClassifyingSpaceBasepoint R) = classifyingSpaceBasepoint G

The comparison of the two models preserves the base points.

@[simp]

theorem TauCeti.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq_cellularHomotopyEquivClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) {G : Type u} [Group G] (e : PresentedGroup R ≃* G) (a : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)) : (classifyingSpaceFundamentalGroupMulEquiv G) ((FundamentalGroup.mapOfEq (cellularHomotopyEquivClassifyingSpace R e).toFun ⋯) a) = e ((cellularClassifyingSpaceFundamentalGroupMulEquiv R) a)

The comparison of the two models induces e on fundamental groups, under the identifications cellularClassifyingSpaceFundamentalGroupMulEquiv R with PresentedGroup R and classifyingSpaceFundamentalGroupMulEquiv G with G.

theorem TauCeti.homotopicRel_cellularHomotopyEquivClassifyingSpace_toFun {S : Type u} (R : Set (FreeGroup S)) {G : Type u} [Group G] (e : PresentedGroup R ≃* G) {f : C(↑(cellularClassifyingSpace R), classifyingSpace G)} (hf : f (cellularClassifyingSpaceBasepoint R) = classifyingSpaceBasepoint G) (hfe : ∀ (a : FundamentalGroup (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)), (classifyingSpaceFundamentalGroupMulEquiv G) ((FundamentalGroup.mapOfEq f hf) a) = e ((cellularClassifyingSpaceFundamentalGroupMulEquiv R) a)) : f.HomotopicRel (cellularHomotopyEquivClassifyingSpace R e).toFun {cellularClassifyingSpaceBasepoint R}

The comparison of the two models is determined by e up to pointed homotopy. Every map from the cellular classifying space to classifyingSpace G that preserves the base points and induces e under the identifications of both fundamental groups is homotopic to it relative to the base point.

theorem TauCeti.exists_path_map_cellularHomotopyEquivClassifyingSpace_invFun {S : Type u} (R : Set (FreeGroup S)) {G : Type u} [Group G] (e : PresentedGroup R ≃* G) : ∃ (γ : Path ((cellularHomotopyEquivClassifyingSpace R e).invFun (classifyingSpaceBasepoint G)) (cellularClassifyingSpaceBasepoint R)), ∀ (a : FundamentalGroup (classifyingSpace G) (classifyingSpaceBasepoint G)), (cellularClassifyingSpaceFundamentalGroupMulEquiv R) ((FundamentalGroup.fundamentalGroupMulEquivOfPath γ) ((FundamentalGroup.map (cellularHomotopyEquivClassifyingSpace R e).invFun (classifyingSpaceBasepoint G)) a)) = e.symm ((classifyingSpaceFundamentalGroupMulEquiv G) a)

The homotopy inverse of the comparison of the two models induces e⁻¹, up to a change of base point: there is a path γ from its value at the base point of classifyingSpace G to the base point of the cellular classifying space such that the induced map, followed by basepoint change along γ, is e⁻¹ under the identifications of both fundamental groups.

instance TauCeti.instSemilocallySimplyConnectedSpaceCellularClassifyingSpace {S : Type u} (R : Set (FreeGroup S)) : SemilocallySimplyConnectedSpace ↑(cellularClassifyingSpace R)

The cellular classifying space is semilocally simply connected. It is homotopy equivalent to Milnor's classifying space of its fundamental group, which is semilocally simply connected, and semilocal simple connectivity is a homotopy invariant.

theorem TauCeti.exists_isEilenbergMacLaneSpaceOne_cellularClassifyingSpace (G : Type u) [Group G] : ∃ (R : Set (FreeGroup G)), LocallyPathConnectedSpace ↑(cellularClassifyingSpace R) ∧ SemilocallySimplyConnectedSpace ↑(cellularClassifyingSpace R) ∧ IsEilenbergMacLaneSpaceOne G (↑(cellularClassifyingSpace R)) (cellularClassifyingSpaceBasepoint R)

Every group has a cellular classifying space, satisfying the standing hypotheses of covering-space theory: for every group G there is a set R of relators on the generators G such that the cellular classifying space of ⟨G | R⟩ is a locally path-connected, semilocally simply connected K(G, 1). Take the tautological presentation, whose relators are the kernel of the evaluation map FreeGroup G →* G. No hypothesis on the group is needed. This is the cellular counterpart of TauCeti.exists_isEilenbergMacLaneSpaceOne.