Naturality of the join-to-standard comparison

A group homomorphism induces an equivariant chain map on the ordered chains of Milnor's countable join. In every degree it relabels each simplex, preserving its increasing-index orientation. The cell maps are those of the continuous maps MonoidHom.universalGSpaceMap, as witnessed by MonoidHom.universalGSpaceMap_characteristicMap.

MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality proves that the explicit comparison with Mathlib's standard complex commutes with these induced maps, as an equality of chain maps of representations. Both routes send a simplex to the tuple of images of its labels. Thus the forward map of TauCeti.universalGSpaceStandardHomotopyEquiv is natural in the group. Restriction of the target action makes the square a square in Rep k G, without any injectivity assumption on the homomorphism.

The join chain maps preserve augmentation by MulActionHom.toRepRes_comp_permutationAugmentation and its reassociated form.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• K. S. Brown, Cohomology of Groups, Springer, 1982, Chapters I and III.

@[reducible, inline]

noncomputable abbrev MonoidHom.universalGSpaceChainHom {k G H : Type u} [Group G] [Group H] [Ring k] (φ : G →* H) (n : ℕ) : Rep.ofMulAction k G ((TauCeti.indexedJoin fun (x : ℕ) => G).RealizationCell n) ⟶ Rep.res φ (Rep.ofMulAction k H ((TauCeti.indexedJoin fun (x : ℕ) => H).RealizationCell n))

Linear extension of relabelling simplices, equivariant along the group homomorphism.

noncomputable def MonoidHom.universalGSpaceChainMap {k G H : Type u} [Group G] [Group H] [Ring k] (φ : G →* H) : TauCeti.universalGSpaceChainComplex k G ⟶ ((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).obj (TauCeti.universalGSpaceChainComplex k H)

The chain map on Milnor join chains induced by a group homomorphism.

@[simp]

theorem MonoidHom.universalGSpaceChainMap_f {k G H : Type u} [Group G] [Group H] [Ring k] (φ : G →* H) (n : ℕ) : φ.universalGSpaceChainMap.f n = φ.universalGSpaceChainHom n

The components of the induced join chain map are the linear extensions of the cell maps.

@[simp]

theorem MonoidHom.universalGSpaceChainMap_id {k G : Type u} [Group G] [Ring k] : (id G).universalGSpaceChainMap = CategoryTheory.CategoryStruct.id (TauCeti.universalGSpaceChainComplex k G)

The identity homomorphism induces the identity map on join chains.

@[simp]

theorem MonoidHom.universalGSpaceChainMap_comp {k G H : Type u} [Group G] [Group H] [Ring k] {K : Type u} [Group K] (ψ : H →* K) (φ : G →* H) : (ψ.comp φ).universalGSpaceChainMap = CategoryTheory.CategoryStruct.comp φ.universalGSpaceChainMap (((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).map ψ.universalGSpaceChainMap)

Join chain maps respect composition, restricting the second map along the first homomorphism.

theorem MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality {k G H : Type u} [Group G] [Group H] [CommRing k] (φ : G →* H) : CategoryTheory.CategoryStruct.comp φ.universalGSpaceChainMap (((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).map (TauCeti.universalGSpaceChainComplexToStandardComplex k H)) = CategoryTheory.CategoryStruct.comp (TauCeti.universalGSpaceChainComplexToStandardComplex k G) φ.standardComplexMap

The join-to-standard comparison is natural in the group. Relabelling simplices before forgetting their indices agrees with first forgetting indices and then relabelling the tuples. This is an equality of chain maps in Rep k G, with target actions restricted along φ.

theorem MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality_assoc {k G H : Type u} [Group G] [Group H] [CommRing k] (φ : G →* H) {Z : ChainComplex (Rep.{u, u, u} k G) ℕ} (h : ((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).obj (Rep.standardComplex k H) ⟶ Z) : CategoryTheory.CategoryStruct.comp φ.universalGSpaceChainMap (CategoryTheory.CategoryStruct.comp (((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).map (TauCeti.universalGSpaceChainComplexToStandardComplex k H)) h) = CategoryTheory.CategoryStruct.comp (TauCeti.universalGSpaceChainComplexToStandardComplex k G) (CategoryTheory.CategoryStruct.comp φ.standardComplexMap h)

The join-to-standard comparison is natural in the group. Relabelling simplices before forgetting their indices agrees with first forgetting indices and then relabelling the tuples. This is an equality of chain maps in Rep k G, with target actions restricted along φ.