The shuffle map on singular chains

For topological spaces X and Y, TopCat.shuffle X Y R S is the Eilenberg--Mac Lane shuffle map from the tensor product of the singular chains of X and Y to the singular chains of X × Y. It is the simplicial shuffle map followed by the chain map induced by the canonical isomorphism Sing X × Sing Y ≅ Sing (X × Y). The construction is natural in both spaces and both coefficient objects.

The comparison with the simplicial shuffle map is recorded in both directions. In particular, composing with the map induced by the two projections recovers the simplicial shuffle map. This places the singular shuffle and Alexander--Whitney maps in the same product comparison and is the input for their Eilenberg--Zilber chain homotopies.

Main definitions and results

• TopCat.shuffle: the shuffle map on singular chains.
• TopCat.shuffle_def: its factorization through the simplicial shuffle map.
• TopCat.ιChainComplex_tensorHom_ιChainComplex_shuffle_f: its value on a pair of singular simplices.
• TopCat.shuffle_naturality: naturality in both spaces.
• TopCat.shuffle_coefficient_naturality: naturality in both coefficient objects.
• TopCat.shuffle_comp_chainComplexMap_prodComparison: projecting a shuffled singular chain recovers the simplicial shuffle map.
• TopCat.shuffle_alexanderWhitney and TopCat.alexanderWhitney_shuffle: the two singular composites expressed through the corresponding simplicial composites.

References

• S. Eilenberg and S. Mac Lane, On the groups H(Π, n), I, Ann. of Math. 58 (1953).
• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).
• C. Weibel, An Introduction to Homological Algebra, Section 8.5.

noncomputable def TopCat.shuffle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) ⟶ (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)

The Eilenberg--Mac Lane shuffle map C(X; R) ⊗ C(Y; S) ⟶ C(X × Y; R ⊗ S) on singular chains: the simplicial shuffle map, followed by the map induced by the monoidal comparison Sing X × Sing Y ⟶ Sing (X × Y).

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.shuffle_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) : X.shuffle Y R S = CategoryTheory.CategoryStruct.comp ((toSSet.obj X).shuffle (toSSet.obj Y) R S) (SSet.chainComplexMap (CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S))

The singular shuffle map is the simplicial shuffle map followed by the chain map induced by the monoidal product comparison Sing X × Sing Y ⟶ Sing (X × Y).

@[simp]

theorem TopCat.ιChainComplex_tensorHom_ιChainComplex_shuffle_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y : TopCat} (R S : C) {p q n : ℕ} (x : (toSSet.obj X).obj (Opposite.op { len := p })) (y : (toSSet.obj Y).obj (Opposite.op { len := q })) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toSSet.obj X).ιChainComplex x) ((toSSet.obj Y).ιChainComplex y)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) ((X.shuffle Y R S).f n)) = CategoryTheory.CategoryStruct.comp (SSet.shuffleChain (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) p q n h) ((SSet.chainComplexMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.yonedaEquiv.symm x) (SSet.yonedaEquiv.symm y)) (CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).f n)

The singular shuffle map on the summand of a p-simplex x of X and a q-simplex y of Y is the image of the shuffle chain under the map to Sing (X × Y) classified by (x, y).

@[simp]

theorem TopCat.ιChainComplex_tensorHom_ιChainComplex_shuffle_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y : TopCat} (R S : C) {p q n : ℕ} (x : (toSSet.obj X).obj (Opposite.op { len := p })) (y : (toSSet.obj Y).obj (Opposite.op { len := q })) (h : p + q = n) {Z : C} (h✝ : ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toSSet.obj X).ιChainComplex x) ((toSSet.obj Y).ιChainComplex y)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) (CategoryTheory.CategoryStruct.comp ((X.shuffle Y R S).f n) h✝)) = CategoryTheory.CategoryStruct.comp (SSet.shuffleChain (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) p q n h) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.yonedaEquiv.symm x) (SSet.yonedaEquiv.symm y)) (CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).f n) h✝)

The singular shuffle map on the summand of a p-simplex x of X and a q-simplex y of Y is the image of the shuffle chain under the map to Sing (X × Y) classified by (x, y).

theorem TopCat.ιChainComplex_tensorHom_ιChainComplex_shuffle_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y : TopCat} (R S : C) (x : (toSSet.obj X).obj (Opposite.op { len := 0 })) (y : (toSSet.obj Y).obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toSSet.obj X).ιChainComplex x) ((toSSet.obj Y).ιChainComplex y)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) 0 0 0 ⋯) ((X.shuffle Y R S).f 0)) = (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y).app (Opposite.op { len := 0 }))) (x, y))

In degree zero, the singular shuffle map sends a pair of singular vertices to the corresponding vertex of the product.

theorem TopCat.shuffle_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map g) S)) (X'.shuffle Y' R S) = CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (SSet.chainComplexMap (toSSet.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S))

The shuffle map on singular chains is natural in both spaces.

theorem TopCat.shuffle_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S : C) {Z : ChainComplex C ℕ} (h : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y')).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map g) S)) (CategoryTheory.CategoryStruct.comp (X'.shuffle Y' R S) h) = CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (toSSet.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) h)

The shuffle map on singular chains is natural in both spaces.

theorem TopCat.shuffle_coefficient_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) {R S R' S' : C} (f : R ⟶ R') (g : S ⟶ S') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((SSet.chainComplexFunctor C).map f).app (toSSet.obj X)) (((SSet.chainComplexFunctor C).map g).app (toSSet.obj Y))) (X.shuffle Y R' S') = CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (((SSet.chainComplexFunctor C).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))

The shuffle map on singular chains is natural in both coefficient objects.

theorem TopCat.shuffle_coefficient_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) {R S R' S' : C} (f : R ⟶ R') (g : S ⟶ S') {Z : ChainComplex C ℕ} (h : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R' S') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((SSet.chainComplexFunctor C).map f).app (toSSet.obj X)) (((SSet.chainComplexFunctor C).map g).app (toSSet.obj Y))) (CategoryTheory.CategoryStruct.comp (X.shuffle Y R' S') h) = CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) h)

The shuffle map on singular chains is natural in both coefficient objects.

theorem TopCat.shuffle_comp_chainComplexMap_prodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) : CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (SSet.chainComplexMap (CategoryTheory.CartesianMonoidalCategory.prodComparison toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) = (toSSet.obj X).shuffle (toSSet.obj Y) R S

Projecting a shuffled singular chain to the product of the two singular simplicial sets recovers the simplicial shuffle map.

theorem TopCat.shuffle_comp_chainComplexMap_prodComparison_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) {Z : ChainComplex C ℕ} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj (toSSet.obj X) (toSSet.obj Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (CategoryTheory.CartesianMonoidalCategory.prodComparison toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) h) = CategoryTheory.CategoryStruct.comp ((toSSet.obj X).shuffle (toSSet.obj Y) R S) h

Projecting a shuffled singular chain to the product of the two singular simplicial sets recovers the simplicial shuffle map.

theorem TopCat.shuffle_alexanderWhitney {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) : CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (X.alexanderWhitney Y R S) = CategoryTheory.CategoryStruct.comp ((toSSet.obj X).shuffle (toSSet.obj Y) R S) ((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S)

The singular composite shuffle ≫ alexanderWhitney is the corresponding simplicial composite, under the canonical identification Sing (X × Y) ≅ Sing X × Sing Y.

theorem TopCat.shuffle_alexanderWhitney_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) h) = CategoryTheory.CategoryStruct.comp ((toSSet.obj X).shuffle (toSSet.obj Y) R S) (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S) h)

The singular composite shuffle ≫ alexanderWhitney is the corresponding simplicial composite, under the canonical identification Sing (X × Y) ≅ Sing X × Sing Y.

theorem TopCat.alexanderWhitney_shuffle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) : CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (X.shuffle Y R S) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (CategoryTheory.CartesianMonoidalCategory.prodComparison toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S) ((toSSet.obj X).shuffle (toSSet.obj Y) R S)) (SSet.chainComplexMap (CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)))

The singular composite alexanderWhitney ≫ shuffle is the simplicial composite conjugated by the canonical product comparison Sing (X × Y) ≅ Sing X × Sing Y.

theorem TopCat.alexanderWhitney_shuffle_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) {Z : ChainComplex C ℕ} (h : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) h) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (CategoryTheory.CartesianMonoidalCategory.prodComparison toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S) (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).shuffle (toSSet.obj Y) R S) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (CategoryTheory.Functor.LaxMonoidal.μ toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) h)))

The singular composite alexanderWhitney ≫ shuffle is the simplicial composite conjugated by the canonical product comparison Sing (X × Y) ≅ Sing X × Sing Y.