Homotopy groups only see the path component of the base point

In positive dimension a generalized loop I^N → X based at x takes all its values in the path component of x, since the cube is path-connected and its boundary, which goes to x, is nonempty (GenLoop.apply_mem_pathComponent). So the map induced on π_N(X, x) by a continuous map depends only on its restriction to that path component (HomotopyGroup.map_eq_of_eqOn_pathComponent), and a subspace containing that path component has the same homotopy groups at x (HomotopyGroup.bijective_map_subtypeVal_of_pathComponent_subset).

In particular, for a disjoint union Σ i, X i the inclusion of the summand X i induces bijections π_N(X i, x) → π_N(Σ i, X i, ⟨i, x⟩) in positive dimension (HomotopyGroup.bijective_map_sigmaMk): it has a retraction (ContinuousMap.sigmaRetraction), collapsing every other summand to x, and the composite the other way round is the identity on the summand, which contains the path component of ⟨i, x⟩. In dimension zero this fails as soon as there is a second nonempty summand. These are the homotopy groups of a CW approximation assembled from one approximation for each path component.

Main results

• GenLoop.apply_mem_pathComponent: a positive-dimensional generalized loop stays in the path component of its base point.
• HomotopyGroup.map_eq_of_eqOn_pathComponent: maps agreeing on the path component of the base point induce the same map on positive-dimensional homotopy groups.
• HomotopyGroup.bijective_map_subtypeVal_of_pathComponent_subset: a subspace containing the path component of the base point has the same positive-dimensional homotopy groups.
• HomotopyGroup.bijective_map_sigmaMk: a summand of a disjoint union has the same positive-dimensional homotopy groups as the disjoint union.

theorem GenLoop.apply_mem_pathComponent {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] (p : ↑(GenLoop N X x)) (t : N → ↑unitInterval) : p t ∈ pathComponent x

In positive dimension a generalized loop based at x takes its values in the path component of x.

theorem GenLoop.map_eq_of_eqOn_pathComponent {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [Nonempty N] {f g : C(X, Y)} (h : Set.EqOn (⇑f) (⇑g) (pathComponent x)) (hf : f x = y) (hg : g x = y) (p : ↑(GenLoop N X x)) : map f hf p = map g hg p

In positive dimension, postcomposing a generalized loop based at x with two maps that agree on the path component of x gives the same generalized loop.

theorem HomotopyGroup.map_eq_of_eqOn_pathComponent {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} [Nonempty N] {f g : C(X, Y)} (h : Set.EqOn (⇑f) (⇑g) (pathComponent x)) (hf : f x = y) (hg : g x = y) : map f hf = map g hg

In positive dimension, the map induced on the homotopy group at x depends only on the values of the continuous map on the path component of x.

theorem HomotopyGroup.bijective_map_subtypeVal_of_pathComponent_subset {N : Type u_1} {X : Type u_2} [TopologicalSpace X] [Nonempty N] {S : Set X} {x : ↑S} {x' : X} (hS : pathComponent ↑x ⊆ S) (hx : ↑x = x') : Function.Bijective (map { toFun := Subtype.val, continuous_toFun := ⋯ } hx)

Homotopy groups of a subspace containing a path component. In positive dimension, if a subspace S contains the path component of x ∈ S, its inclusion induces a bijection π_N(S, x) → π_N(X, x): generalized loops based at x, and homotopies between them relative to the boundary of the cube, take their values in the path component of x.

theorem HomotopyGroup.bijective_map_sigmaMk {N : Type u_1} {ι : Type u_4} {Z : ι → Type u_5} [(i : ι) → TopologicalSpace (Z i)] [Nonempty N] (i : ι) (z : Z i) : Function.Bijective (map (ContinuousMap.sigmaMk i) ⋯)

Homotopy groups of a disjoint union. In positive dimension, the inclusion of a summand Z i into the disjoint union Σ j, Z j induces a bijection on homotopy groups at every point of the summand.