Homotopy groups of totally disconnected spaces

In positive dimensions, every homotopy group of a totally disconnected space is trivial (HomotopyGroup.subsingleton_of_totallyDisconnectedSpace): a generalized loop is constant, since the cube is connected, and it sends the nonempty boundary of the cube to the base point.

Consequently a map f : X → Y out of a totally disconnected space which meets every path component of Y exactly once is a weak homotopy equivalence as soon as the positive-dimensional homotopy groups of Y vanish at the points of its image (ContinuousMap.isWeakHomotopyEquivalence_of_totallyDisconnectedSpace). Taking for X the path components of Y with the discrete topology, this says that a space whose path components are weakly contractible is weakly equivalent to the discrete space of its path components.

Main results

• HomotopyGroup.subsingleton_of_totallyDisconnectedSpace: π_n(X, x) is trivial for a totally disconnected space X and n ≥ 1.
• ContinuousMap.isWeakHomotopyEquivalence_of_totallyDisconnectedSpace: a map from a totally disconnected space meeting each path component of the target exactly once, at points where the positive-dimensional homotopy groups vanish, is a weak homotopy equivalence.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 4.1.

instance HomotopyGroup.subsingleton_of_totallyDisconnectedSpace {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [TotallyDisconnectedSpace X] : Subsingleton (HomotopyGroup N X x)

In positive dimensions, every homotopy group of a totally disconnected space is a subsingleton: a generalized loop is constant, since the cube is connected, and it sends the nonempty boundary of the cube to the base point.

theorem ContinuousMap.isWeakHomotopyEquivalence_of_totallyDisconnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TotallyDisconnectedSpace X] (f : C(X, Y)) (hsurj : ∀ (y : Y), ∃ (x : X), Joined (f x) y) (hinj : ∀ (a b : X), Joined (f a) (f b) → a = b) (hY : ∀ (n : ℕ) (x : X), Subsingleton (HomotopyGroup.Pi (n + 1) Y (f x))) : f.IsWeakHomotopyEquivalence

A map out of a totally disconnected space onto the path components. Let f : X → Y be a map from a totally disconnected space which meets every path component of Y, and meets each of them at most once. If the positive-dimensional homotopy groups of Y vanish at the points of the image of f, then f is a weak homotopy equivalence.