Asphericity and the K(G, 1) property are homotopy invariants

Both properties are stated at a base point, but neither depends on it (TauCeti.IsAspherical.of_basepoint, TauCeti.IsEilenbergMacLaneSpaceOne.of_basepoint): an aspherical space is path connected, so base-point change identifies its homotopy groups at any two points. With that, homotopy invariance follows from the invariance of the homotopy groups themselves, since a homotopy equivalence carries no base point with it.

These are the canonical invariance statements for both properties. In particular they cover a homeomorphism e : X ≃ₜ Y, through e.toHomotopyEquiv, at any base point of Y.

Main declarations

• TauCeti.IsAspherical.of_homotopyEquiv: asphericity is a homotopy invariant.
• TauCeti.IsEilenbergMacLaneSpaceOne.of_homotopyEquiv: being a K(G, 1) space is a homotopy invariant.

References

Compare Section 1.B of [hatcher02].

theorem TauCeti.IsAspherical.of_homotopyEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} (h : IsAspherical X x) (e : ContinuousMap.HomotopyEquiv X Y) (y : Y) : IsAspherical Y y

Asphericity is a homotopy invariant. A space homotopy equivalent to an aspherical space is aspherical, at every base point.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.of_homotopyEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {G : Type u_3} [Group G] (h : IsEilenbergMacLaneSpaceOne G X x) (e : ContinuousMap.HomotopyEquiv X Y) (y : Y) : IsEilenbergMacLaneSpaceOne G Y y

Being an Eilenberg--Mac Lane space of type K(G, 1) is a homotopy invariant.