Strict functoriality of Milnor's classifying spaces

A group homomorphism induces a continuous map of classifying spaces by applying it to the labels of the countable join and descending to orbits. These maps preserve the chosen base points and respect identity homomorphisms and composition as equalities of continuous maps. The total-space maps are equivariant, so the orbit projections commute with the induced maps.

The representative formula MonoidHom.classifyingSpaceMap_proj characterizes the induced map without unfolding the orbit space. Together with classifyingSpace_continuousMap_ext, it also lets callers prove identities of induced maps on representatives.

Under the identifications classifyingSpaceFundamentalGroupMulEquiv of the fundamental groups of the classifying spaces with the groups themselves, the map induced on fundamental groups is the original homomorphism.

Main definitions

• MonoidHom.classifyingSpaceMap: the continuous map induced by a group homomorphism.

Main results

• MonoidHom.classifyingSpaceMap_proj: compatibility with the orbit projections.
• MonoidHom.classifyingSpaceMap_basepoint: preservation of the chosen base points.
• MonoidHom.classifyingSpaceMap_id, MonoidHom.classifyingSpaceMap_comp: strict functor laws.
• MonoidHom.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq: the induced map on fundamental groups is the original homomorphism.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 1.B.

noncomputable def MonoidHom.classifyingSpaceMap {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) : C(TauCeti.classifyingSpace G, TauCeti.classifyingSpace H)

A group homomorphism induces a continuous map of Milnor classifying spaces by applying it to the vertex labels of the countable join and passing to orbits.

@[simp]

theorem MonoidHom.classifyingSpaceMap_proj {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) (x : TauCeti.universalGSpace G) : φ.classifyingSpaceMap (TauCeti.classifyingSpaceProj G x) = TauCeti.classifyingSpaceProj H (φ.universalGSpaceMap x)

The induced map commutes with the orbit projections.

@[simp]

theorem MonoidHom.classifyingSpaceMap_basepoint {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) : φ.classifyingSpaceMap (TauCeti.classifyingSpaceBasepoint G) = TauCeti.classifyingSpaceBasepoint H

The induced map preserves the chosen base point.

@[simp]

theorem MonoidHom.classifyingSpaceMap_id {G : Type u} [Group G] : (id G).classifyingSpaceMap = ContinuousMap.id (TauCeti.classifyingSpace G)

The identity homomorphism induces the identity continuous map.

@[simp]

theorem MonoidHom.classifyingSpaceMap_comp {G : Type u} {H : Type v} {K : Type w} [Group G] [Group H] [Group K] (ψ : H →* K) (φ : G →* H) : (ψ.comp φ).classifyingSpaceMap = ψ.classifyingSpaceMap.comp φ.classifyingSpaceMap

Composition of group homomorphisms induces composition of continuous maps, strictly.

@[simp]

theorem MonoidHom.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq {G : Type u} {H : Type v} [Group G] [Group H] (φ : G →* H) (γ : FundamentalGroup (TauCeti.classifyingSpace G) (TauCeti.classifyingSpaceBasepoint G)) : (TauCeti.classifyingSpaceFundamentalGroupMulEquiv H) ((FundamentalGroup.mapOfEq φ.classifyingSpaceMap ⋯) γ) = φ ((TauCeti.classifyingSpaceFundamentalGroupMulEquiv G) γ)

The induced map on fundamental groups is the homomorphism itself. Under the identifications classifyingSpaceFundamentalGroupMulEquiv of the fundamental groups of the classifying spaces with G and H, the map induced by φ.classifyingSpaceMap on fundamental groups at the base points is φ.