The universal cover of an aspherical CW complex is contractible

Let p : E → B be a covering map. If B carries a CW structure on the whole space and is aspherical, and E is simply connected, then E is weakly contractible (IsCoveringMap.subsingleton_homotopyGroup_of_isAspherical). It has CW type through the lifted CW structure TauCeti.cwComplexPreimage, so it is contractible by Whitehead's theorem (TauCeti.contractibleSpace_of_subsingleton_homotopyGroup).

This is the contractibility needed to apply the cellular projective resolution TauCeti.cellularResolution to the universal cover of a K(G, 1) CW complex.

Main results

• IsCoveringMap.contractibleSpace_of_isAspherical: the simply connected cover of an aspherical CW complex is contractible.
• IsCoveringMap.contractibleSpace_preimage_univ_of_isAspherical: the same for the lift p ⁻¹' univ of the CW structure on the whole base.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 4.1, Theorem 4.5 and the corollary after it.

theorem IsCoveringMap.contractibleSpace_of_isAspherical {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {e : E} {b : B} (hp : IsCoveringMap p) [T2Space B] [Topology.CWComplex Set.univ] [SimplyConnectedSpace E] (he : p e = b) (hb : TauCeti.IsAspherical B b) : ContractibleSpace E

The simply connected cover of an aspherical CW complex is contractible. If B carries a CW structure on the whole space and is aspherical at a point b lifting to e, and E is simply connected, then E is weakly contractible; it has CW type, through the lifted CW structure, so it is contractible by Whitehead's theorem.

theorem IsCoveringMap.contractibleSpace_preimage_univ_of_isAspherical {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {e : E} {b : B} (hp : IsCoveringMap p) [T2Space B] [Topology.CWComplex Set.univ] [SimplyConnectedSpace E] (he : p e = b) (hb : TauCeti.IsAspherical B b) : ContractibleSpace ↑(p ⁻¹' Set.univ)

The lift of an aspherical CW complex to a simply connected cover is contractible: the form of IsCoveringMap.contractibleSpace_of_isAspherical for p ⁻¹' univ, the space carrying the lifted CW structure.