Path connectedness is a homotopy invariant

A homotopy equivalence e : X ≃ₕ Y is not surjective, so path connectedness of Y cannot be read off from the image of a path in X. What replaces surjectivity is the trace of the homotopy e.toFun ∘ e.invFun ≃ id: evaluated at a point y, it is a path from e.toFun (e.invFun y) to y. Two points of Y are therefore joined to points in the image of e.toFun, which are joined to each other because X is path connected.

This is the prerequisite for the base-point-free homotopy-group statements in TauCeti.Topology.Homotopy.HomotopyGroup.HomotopyEquiv, which need the target space to be path connected before base-point change is available there.

Main declarations

• ContinuousMap.HomotopyEquiv.pathConnectedSpace: a space homotopy equivalent to a path connected space is path connected.

theorem ContinuousMap.HomotopyEquiv.pathConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PathConnectedSpace X] (e : HomotopyEquiv X Y) : PathConnectedSpace Y

Path connectedness is a homotopy invariant. A space homotopy equivalent to a path connected space is path connected.