The countable join model for a universal group space

Specializing the indexed join to the constant family on ℕ gives universalGSpace G, the underlying space in Milnor's join construction. The distinguished vertex over index zero supplies its base point when G has a chosen unit. Later constructions can define the diagonal group action directly on these labelled vertices. Homomorphisms induce continuous maps preserving the base point and respecting identities and composition.

Main definitions

• TauCeti.universalGSpace: the realization of the countable join of copies of G.
• TauCeti.universalGSpaceBasepoint: the distinguished vertex over index zero.
• MonoidHom.universalGSpaceMap: the map induced by a homomorphism.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

@[reducible, inline]

abbrev TauCeti.universalGSpace (G : Type u) : Type u

Milnor's countable join of copies of a type, realized with the weak topology.

noncomputable def TauCeti.universalGSpaceBasepoint (G : Type u) [One G] : universalGSpace G

The distinguished vertex over index zero in the countable join of copies of a type with a chosen unit.

@[simp]

theorem TauCeti.universalGSpaceBasepoint_val (G : Type u) [One G] : ↑(universalGSpaceBasepoint G) = Finsupp.single ⟨0, 1⟩ 1

The barycentric coordinates of the distinguished point are concentrated at the vertex labelled by index zero and the chosen unit.

noncomputable def MonoidHom.universalGSpaceMap {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) : C(TauCeti.universalGSpace G, TauCeti.universalGSpace H)

A homomorphism induces a continuous map of Milnor total spaces by applying it to vertex labels and leaving indices unchanged.

@[simp]

theorem MonoidHom.universalGSpaceMap_val {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) (x : TauCeti.universalGSpace G) : ↑(φ.universalGSpaceMap x) = Finsupp.mapDomain (fun (v : (_ : ℕ) × G) => ⟨v.fst, φ v.snd⟩) ↑x

The induced map pushes forward barycentric coordinates.

@[simp]

theorem MonoidHom.universalGSpaceMap_basepoint {G : Type u} {H : Type v} [MulOne G] [MulOne H] (φ : G →* H) : φ.universalGSpaceMap (TauCeti.universalGSpaceBasepoint G) = TauCeti.universalGSpaceBasepoint H

The map induced by a homomorphism preserves the distinguished base point.

@[simp]

theorem MonoidHom.universalGSpaceMap_id {G : Type u} [MulOne G] : (id G).universalGSpaceMap = ContinuousMap.id (TauCeti.universalGSpace G)

The induced continuous map respects identities.

@[simp]

theorem MonoidHom.universalGSpaceMap_comp {G : Type u} {H : Type v} [MulOne G] [MulOne H] {K : Type u_1} [MulOne K] (ψ : H →* K) (φ : G →* H) : (ψ.comp φ).universalGSpaceMap = ψ.universalGSpaceMap.comp φ.universalGSpaceMap

The induced continuous map respects composition.