Weak contractibility of the countable join

An indexed join is weakly contractible when nonempty family members occur at infinitely many indices (AlgebraicTopology/SimplicialComplex/Join/WeakContractibility.lean). This file specializes those facts to Milnor's countable join universalGSpace, whose family members are all nonempty as soon as G is.

Main results

• TauCeti.instSimplyConnectedSpaceUniversalGSpace: simple connectedness of the countable join.
• TauCeti.subsingleton_homotopyGroup_universalGSpace: all its positive-dimensional homotopy groups vanish.
• ContinuousMap.nullhomotopic_to_universalGSpace: every map from a compact space to it is nullhomotopic.

instance TauCeti.instSimplyConnectedSpaceUniversalGSpace (G : Type u) [Nonempty G] : SimplyConnectedSpace (universalGSpace G)

Milnor's countable join of a nonempty type is simply connected.

theorem TauCeti.subsingleton_homotopyGroup_universalGSpace (G : Type u) (n : ℕ) (x : universalGSpace G) : Subsingleton (HomotopyGroup.Pi (n + 1) (universalGSpace G) x)

Every positive-dimensional homotopy group of Milnor's countable join is trivial.

theorem ContinuousMap.nullhomotopic_to_universalGSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] {G : Type u} [Nonempty G] (f : C(X, TauCeti.universalGSpace G)) : f.Nullhomotopic

Every map from a compact space to Milnor's countable join is nullhomotopic.