Weak homotopy equivalences between aspherical and Eilenberg--Mac Lane spaces

An aspherical space is path-connected and its homotopy groups vanish in every dimension except one, so the only homotopy invariant a map between aspherical spaces can fail to preserve is the fundamental group. Accordingly, a map between aspherical spaces is a weak homotopy equivalence exactly when it induces an isomorphism of fundamental groups at one base point (TauCeti.IsAspherical.isWeakHomotopyEquivalence_iff).

Combined with Whitehead's theorem ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv, this is the last step in the uniqueness of K(G, 1) spaces: a map between two K(G, 1) spaces of CW type that induces an isomorphism of fundamental groups is a homotopy equivalence. The hypothesis on both spaces cannot be dropped, because the Warsaw circle and a point are both aspherical with trivial fundamental group, but they are not homotopy equivalent.

In the same way, a map between Eilenberg--Mac Lane spaces in the same degree n is a weak homotopy equivalence exactly when it induces a bijection on πₙ at one base point (TauCeti.IsEilenbergMacLaneSpace.isWeakHomotopyEquivalence_iff), so by Whitehead's theorem such a map between two K(G, n) spaces of CW type is a homotopy equivalence.

Main results

• TauCeti.IsAspherical.isWeakHomotopyEquivalence_iff: a map between aspherical spaces is a weak homotopy equivalence exactly when it induces a bijection of fundamental groups.
• TauCeti.IsEilenbergMacLaneSpace.isWeakHomotopyEquivalence_iff: a map between K(G, n) and K(H, n) spaces is a weak homotopy equivalence exactly when it is bijective on πₙ.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 1.B, Theorem 1B.8, Section 4.1, Theorem 4.5, and Section 4.2, Proposition 4.30.

theorem TauCeti.IsAspherical.isWeakHomotopyEquivalence_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {f : C(X, Y)} (hX : IsAspherical X x) (hY : IsAspherical Y y) (hxy : f x = y) : f.IsWeakHomotopyEquivalence ↔ Function.Bijective ⇑(FundamentalGroup.mapOfEq f hxy)

A map between aspherical spaces is a weak homotopy equivalence exactly when it induces an isomorphism of fundamental groups. Bijectivity at the single base point x suffices.

theorem TauCeti.IsEilenbergMacLaneSpace.isWeakHomotopyEquivalence_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] {n : ℕ} [NeZero n] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (hX : IsEilenbergMacLaneSpace G n X x) (hY : IsEilenbergMacLaneSpace H n Y y) {f : C(X, Y)} (hxy : f x = y) : f.IsWeakHomotopyEquivalence ↔ Function.Bijective (HomotopyGroup.map f hxy)

A map between Eilenberg--Mac Lane spaces in the same degree is a weak homotopy equivalence exactly when it induces a bijection on πₙ. Bijectivity at the single base point x suffices, and the groups G and H play no role.