Weak contractibility of indexed joins #
Every map from a compact space into an indexed join uses only finitely many vertices. If nonempty members occur at infinitely many indices, a vertex over an unused index turns that finite restriction into a cone. This gives a nullhomotopy of the map inside the full join. Applied to the inclusions of the images of loops and of cubes, it shows that such a join is weakly contractible.
Main results #
ContinuousMap.nullhomotopic_to_indexedJoin: every map with compact image to such an indexed join is nullhomotopic.TauCeti.pathConnectedSpace_realization_indexedJoin: path-connectedness of the indexed join.TauCeti.simplyConnectedSpace_realization_indexedJoin: simple connectedness.TauCeti.subsingleton_homotopyGroup_realization_indexedJoin: vanishing homotopy groups.
theorem
ContinuousMap.nullhomotopic_to_indexedJoin
{ι : Type u}
{A : ι → Type v}
{X : Type w}
[TopologicalSpace X]
(f : C(X, (TauCeti.indexedJoin A).Realization))
(hf : IsCompact (Set.range ⇑f))
(hA : {i : ι | Nonempty (A i)}.Infinite)
:
Every continuous map with compact image into an indexed join is nullhomotopic when nonempty family members occur at infinitely many indices.
theorem
TauCeti.subsingleton_homotopyGroup_realization_indexedJoin
{ι : Type u}
{A : ι → Type v}
(hA : {i : ι | Nonempty (A i)}.Infinite)
(N : Type u_1)
[Finite N]
[Nonempty N]
(x : (indexedJoin A).Realization)
:
Subsingleton (HomotopyGroup N (indexedJoin A).Realization x)
Every positive-dimensional homotopy group of an indexed join is trivial if nonempty family members occur at infinitely many indices.