Semilocal simple connectivity is a homotopy invariant

If X and Y are homotopy equivalent, then X is semilocally simply connected if and only if Y is. The forward map f of a homotopy equivalence X ≃ₕ Y induces an injective map π₁(X, x) → π₁(Y, f x) at every point (ContinuousMap.HomotopyEquiv.fundamentalGroup_map_bijective), so the preimage under f of a neighbourhood of f x whose loops are null-homotopic in Y is a neighbourhood of x whose loops are null-homotopic in X (TauCeti.SemilocallySimplyConnectedSpace.of_map_injective).

This lets the standing hypotheses of covering-space theory be transported along homotopy equivalences, for instance from one model of a classifying space to another. Unlike semilocal simple connectivity, local path-connectedness is not a homotopy invariant: the comb space is contractible but not locally path-connected.

Main results

• ContinuousMap.HomotopyEquiv.semilocallySimplyConnectedSpace: a space homotopy equivalent to a semilocally simply connected space is semilocally simply connected.
• ContinuousMap.HomotopyEquiv.semilocallySimplyConnectedSpace_iff: the iff form.

theorem ContinuousMap.HomotopyEquiv.semilocallySimplyConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TauCeti.SemilocallySimplyConnectedSpace Y] (e : HomotopyEquiv X Y) : TauCeti.SemilocallySimplyConnectedSpace X

A space homotopy equivalent to a semilocally simply connected space is semilocally simply connected.

theorem ContinuousMap.HomotopyEquiv.semilocallySimplyConnectedSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : TauCeti.SemilocallySimplyConnectedSpace X ↔ TauCeti.SemilocallySimplyConnectedSpace Y

Semilocal simple connectivity is a homotopy invariant.