The shuffle map

Let C be a preadditive monoidal category with w-small coproducts, in which tensoring on either side preserves w-small coproducts (for instance ModuleCat k). For simplicial sets K and L and objects R and S of C, the shuffle map of Eilenberg and Mac Lane is the morphism of chain complexes SSet.shuffle K L R S from K.chainComplex R ⊗ L.chainComplex S, the tensor product of the simplicial chains of the factors, to (K ⊗ L).chainComplex (R ⊗ S), the simplicial chains of the product K × L. The tensor product of chain complexes is Mathlib's monoidal structure on ChainComplex C ℕ, whose differential is d (a ⊗ b) = d a ⊗ b + (-1)^p a ⊗ d b for a of degree p. The shuffle map is the other half, besides the Alexander–Whitney map SSet.alexanderWhitney, of the Eilenberg–Zilber comparison between chains on a product and tensor products of chains.

The shuffle map is first constructed on the standard simplices. The shuffle chain SSet.shuffleChain T p q (p + q) is a (p + q)-chain of Δ[p] ⊗ Δ[q] with coefficients in T. Unwinding its recursion, it is the signed sum of the nondegenerate (p + q)-simplices of Δ[p] ⊗ Δ[q]: the monotone lattice paths from (0, 0) to (p, q), each with the sign (-1)^N, where N counts the pairs of a vertical step followed, later on the path, by a horizontal step. Here a path is built from its first step: either a horizontal step (0, 0) → (1, 0) followed by a path from (1, 0), or a vertical step (0, 0) → (0, 1) followed by a path from (0, 1) with the sign (-1)^p. The two cases are the cone from (0, 0) (SSet.stdSimplex.prodConeChain) on the shuffle chains of Δ[p - 1] ⊗ Δ[q] and Δ[p] ⊗ Δ[q - 1], pushed along the zeroth face maps. The shuffle map then sends the summand of a p-simplex x of K and a q-simplex y of L to the image of the shuffle chain under the map Δ[p] ⊗ Δ[q] ⟶ K ⊗ L classifying (x, y) (SSet.ιChainComplex_tensorHom_ιChainComplex_shuffle_f). This is the classical formula x ⊗ y ↦ ∑ ± (s_ν x, s_μ y) over the (p, q)-shuffles (μ, ν), although this file works with the recursion and does not state that closed formula.

The boundary of the cone is ∂ (c σ) = σ - c (∂ σ) in positive degrees (SSet.stdSimplex.prodConeChain_d). An induction on the degree then shows that the boundary of the shuffle chain is the alternating sum of its faces in the first factor plus (-1)^p times the alternating sum of its faces in the second factor, which is exactly the statement that the shuffle map is a morphism of chain complexes.

Main definitions and results

• SSet.stdSimplex.coneChain: the cone from the vertex 0 on the simplicial chains of Δ[a], with SSet.stdSimplex.coneChain_d and SSet.stdSimplex.coneChain_zero_d its boundary formulas.
• SSet.stdSimplex.prodConeChain: the cone from the vertex (0, 0) on the simplicial chains of Δ[a] ⊗ Δ[b], with SSet.stdSimplex.prodConeChain_d its boundary formula.
• SSet.shuffleChain: the shuffle chain of Δ[p] ⊗ Δ[q], with its defining recursion SSet.shuffleChain_zero_zero, SSet.shuffleChain_succ_zero, SSet.shuffleChain_zero_succ and SSet.shuffleChain_succ_succ, its boundary formula SSet.shuffleChain_d_succ_succ, SSet.shuffleChain_d_succ_zero and SSet.shuffleChain_d_zero_succ, and its naturality in the coefficient object.
• SSet.shuffle: the shuffle map, a morphism of chain complexes.
• SSet.ιChainComplex_tensorHom_ιChainComplex_shuffle_f: its value on the summand of a pair of simplices, and SSet.ιChainComplex_tensorHom_ιChainComplex_shuffle_f_zero in degree zero.
• SSet.shuffle_naturality: it is natural in both simplicial sets.
• SSet.shuffle_coefficient_naturality: it is natural in both coefficient objects.

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.

def SSet.stdSimplex.cone {a m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m + 1 })

The cone from the vertex 0 on a simplex x of the standard simplex Δ[a]: the simplex whose vertices are 0, x 0, …, x m.

Equations

• SSet.stdSimplex.cone x = SSet.stdSimplex.objMk { toFun := Matrix.vecCons 0 ⇑x, monotone' := ⋯ }

@[simp]

theorem SSet.stdSimplex.cone_apply_zero {a m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) : (cone x) 0 = 0

@[simp]

theorem SSet.stdSimplex.cone_apply_succ {a m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) (i : Fin (m + 1)) : (cone x) i.succ = x i

@[simp]

theorem SSet.stdSimplex.δ_zero_cone {a m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := a }) 0)) (cone x) = x

The zeroth face of the cone on x is x.

@[simp]

theorem SSet.stdSimplex.δ_succ_cone {a m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m + 1 })) (i : Fin (m + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := a }) i.succ)) (cone x) = cone ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := a }) i)) x)

The (i + 1)-st face of the cone on x is the cone on the i-th face of x.

theorem SSet.stdSimplex.δ_one_cone {a : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := 0 })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := a }) 1)) (cone x) = const a 0 (Opposite.op { len := 0 })

The second face (index 1) of the cone on a vertex x is the vertex 0.

theorem SSet.stdSimplex.map_cone {a b m : ℕ} (g : { len := a } ⟶ { len := b }) (hg : (SimplexCategory.Hom.toOrderHom g) 0 = 0) (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) : (CategoryTheory.ConcreteCategory.hom ((stdSimplex.map g).app (Opposite.op { len := m + 1 }))) (cone x) = cone ((CategoryTheory.ConcreteCategory.hom ((stdSimplex.map g).app (Opposite.op { len := m }))) x)

A map of standard simplices which fixes the vertex 0 commutes with cones.

def SSet.stdSimplex.prodCone {a b m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m + 1 })

The cone from the vertex (0, 0) on a simplex of the product Δ[a] ⊗ Δ[b].

Equations

• SSet.stdSimplex.prodCone x = (SSet.stdSimplex.cone x.1, SSet.stdSimplex.cone x.2)

theorem SSet.stdSimplex.δ_zero_prodCone {a b m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })) 0)) (prodCone x) = x

The zeroth face of the cone on a simplex x of Δ[a] ⊗ Δ[b] is x.

theorem SSet.stdSimplex.δ_succ_prodCone {a b m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m + 1 })) (i : Fin (m + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })) i.succ)) (prodCone x) = prodCone ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })) i)) x)

The (i + 1)-st face of the cone on a simplex x of Δ[a] ⊗ Δ[b] is the cone on the i-th face of x.

noncomputable def SSet.stdSimplex.coneChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) (m : ℕ) : ((stdSimplex.obj { len := a }).chainComplex T).X m ⟶ ((stdSimplex.obj { len := a }).chainComplex T).X (m + 1)

The cone from the vertex 0, as a map raising the degree of the simplicial chains of Δ[a] by one. It is a contracting homotopy in positive degrees (SSet.stdSimplex.coneChain_d), and in degree zero it contracts onto the vertex 0 (SSet.stdSimplex.coneChain_zero_d).

Equations

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

@[simp]

theorem SSet.stdSimplex.ιChainComplex_coneChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) {m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) : CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex x) (coneChain a T m) = (stdSimplex.obj { len := a }).ιChainComplex (cone x)

@[simp]

theorem SSet.stdSimplex.ιChainComplex_coneChain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) {m : ℕ} (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := m })) {Z : C} (h : ((stdSimplex.obj { len := a }).chainComplex T).X (m + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex x) (CategoryTheory.CategoryStruct.comp (coneChain a T m) h) = CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex (cone x)) h

theorem SSet.stdSimplex.coneChain_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) (m : ℕ) : CategoryTheory.CategoryStruct.comp (coneChain a T (m + 1)) (((stdSimplex.obj { len := a }).chainComplex T).d (m + 1 + 1) (m + 1)) = CategoryTheory.CategoryStruct.id (((stdSimplex.obj { len := a }).chainComplex T).X (m + 1)) - CategoryTheory.CategoryStruct.comp (((stdSimplex.obj { len := a }).chainComplex T).d (m + 1) m) (coneChain a T m)

The cone on the simplicial chains of Δ[a] is a contracting homotopy in positive degrees: ∂ (c ∘ σ) = σ - c ∘ ∂ σ for a chain σ of positive degree.

noncomputable def SSet.stdSimplex.constZeroChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) : ((stdSimplex.obj { len := a }).chainComplex T).X 0 ⟶ ((stdSimplex.obj { len := a }).chainComplex T).X 0

The map on the 0-chains of Δ[a] which sends the summand of every vertex to the summand of the vertex 0.

Equations

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

@[simp]

theorem SSet.stdSimplex.ιChainComplex_constZeroChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := 0 })) : CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex x) (constZeroChain a T) = (stdSimplex.obj { len := a }).ιChainComplex (const a 0 (Opposite.op { len := 0 }))

@[simp]

theorem SSet.stdSimplex.ιChainComplex_constZeroChain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) (x : (stdSimplex.obj { len := a }).obj (Opposite.op { len := 0 })) {Z : C} (h : ((stdSimplex.obj { len := a }).chainComplex T).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex x) (CategoryTheory.CategoryStruct.comp (constZeroChain a T) h) = CategoryTheory.CategoryStruct.comp ((stdSimplex.obj { len := a }).ιChainComplex (const a 0 (Opposite.op { len := 0 }))) h

theorem SSet.stdSimplex.coneChain_zero_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) : CategoryTheory.CategoryStruct.comp (coneChain a T 0) (((stdSimplex.obj { len := a }).chainComplex T).d 1 0) = CategoryTheory.CategoryStruct.id (((stdSimplex.obj { len := a }).chainComplex T).X 0) - constZeroChain a T

In degree zero, the boundary of the cone on a vertex x is x minus the vertex 0.

@[simp]

theorem SSet.stdSimplex.d_constZeroChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) : CategoryTheory.CategoryStruct.comp (((stdSimplex.obj { len := a }).chainComplex T).d 1 0) (constZeroChain a T) = 0

Collapsing every vertex onto the vertex 0 kills boundaries.

@[simp]

theorem SSet.stdSimplex.d_constZeroChain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a : ℕ) (T : C) {Z : C} (h : ((stdSimplex.obj { len := a }).chainComplex T).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (((stdSimplex.obj { len := a }).chainComplex T).d 1 0) (CategoryTheory.CategoryStruct.comp (constZeroChain a T) h) = CategoryTheory.CategoryStruct.comp 0 h

Collapsing every vertex onto the vertex 0 kills boundaries.

noncomputable def SSet.stdSimplex.prodConeChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) (m : ℕ) : ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).X m ⟶ ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).X (m + 1)

The cone from the vertex (0, 0), as a map raising the degree of the simplicial chains of Δ[a] ⊗ Δ[b] by one. It is a contracting homotopy in positive degrees (SSet.stdSimplex.prodConeChain_d).

Equations

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

@[simp]

theorem SSet.stdSimplex.ιChainComplex_prodConeChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) {m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).ιChainComplex x) (prodConeChain a b T m) = (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).ιChainComplex (prodCone x)

@[simp]

theorem SSet.stdSimplex.ιChainComplex_prodConeChain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) {m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })) {Z : C} (h : ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).X (m + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).ιChainComplex x) (CategoryTheory.CategoryStruct.comp (prodConeChain a b T m) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).ιChainComplex (prodCone x)) h

theorem SSet.stdSimplex.prodConeChain_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) (m : ℕ) : CategoryTheory.CategoryStruct.comp (prodConeChain a b T (m + 1)) (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).d (m + 1 + 1) (m + 1)) = CategoryTheory.CategoryStruct.id (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).X (m + 1)) - CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).chainComplex T).d (m + 1) m) (prodConeChain a b T m)

The cone on the simplicial chains of Δ[a] ⊗ Δ[b] is a contracting homotopy in positive degrees: ∂ (c ∘ σ) = σ - c ∘ ∂ σ for a chain σ of positive degree.

theorem SSet.stdSimplex.chainComplexMap_f_prodConeChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {a b : ℕ} (T : C) {a' b' : ℕ} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a' }) (stdSimplex.obj { len := b' })) (hf : ∀ (m : ℕ) (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })), (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := m + 1 }))) (prodCone x) = prodCone ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := m }))) x)) (m : ℕ) : CategoryTheory.CategoryStruct.comp ((chainComplexMap f T).f m) (prodConeChain a' b' T m) = CategoryTheory.CategoryStruct.comp (prodConeChain a b T m) ((chainComplexMap f T).f (m + 1))

A map of products of standard simplices which commutes with the cones commutes with the cone on simplicial chains.

theorem SSet.stdSimplex.chainComplexMap_f_prodConeChain_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {a b : ℕ} (T : C) {a' b' : ℕ} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a' }) (stdSimplex.obj { len := b' })) (hf : ∀ (m : ℕ) (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b })).obj (Opposite.op { len := m })), (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := m + 1 }))) (prodCone x) = prodCone ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := m }))) x)) (m : ℕ) {Z : C} (h : ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a' }) (stdSimplex.obj { len := b' })).chainComplex T).X (m + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((chainComplexMap f T).f m) (CategoryTheory.CategoryStruct.comp (prodConeChain a' b' T m) h) = CategoryTheory.CategoryStruct.comp (prodConeChain a b T m) (CategoryTheory.CategoryStruct.comp ((chainComplexMap f T).f (m + 1)) h)

A map of products of standard simplices which commutes with the cones commutes with the cone on simplicial chains.

theorem SSet.stdSimplex.prodConeChain_chainComplexFunctor_map_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) {T' : C} (u : T ⟶ T') (m : ℕ) : CategoryTheory.CategoryStruct.comp (prodConeChain a b T m) ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }))).f (m + 1)) = CategoryTheory.CategoryStruct.comp ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }))).f m) (prodConeChain a b T' m)

The cone on simplicial chains of Δ[a] ⊗ Δ[b] is natural in the coefficient object.

theorem SSet.stdSimplex.prodConeChain_chainComplexFunctor_map_app_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (a b : ℕ) (T : C) {T' : C} (u : T ⟶ T') (m : ℕ) {Z : C} (h : (((chainComplexFunctor C).obj T').obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }))).X (m + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (prodConeChain a b T m) (CategoryTheory.CategoryStruct.comp ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }))).f (m + 1)) h) = CategoryTheory.CategoryStruct.comp ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := a }) (stdSimplex.obj { len := b }))).f m) (CategoryTheory.CategoryStruct.comp (prodConeChain a b T' m) h)

The cone on simplicial chains of Δ[a] ⊗ Δ[b] is natural in the coefficient object.

def SSet.shuffleChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (p q n : ℕ) : p + q = n → (T ⟶ ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := q })).chainComplex T).X n)

The shuffle chain of Δ[p] ⊗ Δ[q] with coefficients in T, a chain of degree n = p + q. It is defined by recursion on the first step of a lattice path from (0, 0) to (p, q): the shuffle chain of Δ[0] ⊗ Δ[0] is its unique vertex (SSet.shuffleChain_zero_zero), and otherwise it is the cone from (0, 0) on the shuffle chain of Δ[p - 1] ⊗ Δ[q] pushed along the zeroth face Δ[p - 1] ⟶ Δ[p], plus (-1)^p times the cone on the shuffle chain of Δ[p] ⊗ Δ[q - 1] pushed along the zeroth face Δ[q - 1] ⟶ Δ[q], where a term is absent when the corresponding index is zero (SSet.shuffleChain_succ_zero, SSet.shuffleChain_zero_succ and SSet.shuffleChain_succ_succ).

Equations

• One or more equations did not get rendered due to their size.
• SSet.shuffleChain T 0 0 0 x_4 = (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := 0 }) (SSet.stdSimplex.obj { len := 0 })).ιChainComplex SSet.vertex✝
• SSet.shuffleChain T 0 0 n.succ h = absurd h ⋯
• SSet.shuffleChain T n.succ x✝ 0 h = absurd h ⋯
• SSet.shuffleChain T 0 n.succ 0 h = absurd h ⋯

theorem SSet.shuffleChain_chainComplexFunctor_map_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {T T' : C} (u : T ⟶ T') (p q n : ℕ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (shuffleChain T p q n h) ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := q }))).f n) = CategoryTheory.CategoryStruct.comp u (shuffleChain T' p q n h)

The shuffle chain is natural in the coefficient object.

theorem SSet.shuffleChain_chainComplexFunctor_map_app_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {T T' : C} (u : T ⟶ T') (p q n : ℕ) (h : p + q = n) {Z : C} (h✝ : (((chainComplexFunctor C).obj T').obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := q }))).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (shuffleChain T p q n h) (CategoryTheory.CategoryStruct.comp ((((chainComplexFunctor C).map u).app (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p }) (stdSimplex.obj { len := q }))).f n) h✝) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (shuffleChain T' p q n h) h✝)

The shuffle chain is natural in the coefficient object.

theorem SSet.shuffleChain_zero_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (h : 0 + 0 = 0) (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })).obj (Opposite.op { len := 0 })) : shuffleChain T 0 0 0 h = (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := 0 })).ιChainComplex x

The shuffle chain of Δ[0] ⊗ Δ[0] is its unique vertex.

theorem SSet.shuffleChain_succ_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (p n : ℕ) (h : p + 1 + 0 = n + 1) : shuffleChain T (p + 1) 0 (n + 1) h = CategoryTheory.CategoryStruct.comp (shuffleChain T p 0 n ⋯) (CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight (stdSimplex.δ 0) (stdSimplex.obj { len := 0 })) T).f n) (stdSimplex.prodConeChain (p + 1) 0 T n))

The shuffle chain of Δ[p + 1] ⊗ Δ[0] is the cone on the shuffle chain of Δ[p] ⊗ Δ[0], pushed along the zeroth face of Δ[p + 1].

theorem SSet.shuffleChain_zero_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (q n : ℕ) (h : 0 + (q + 1) = n + 1) : shuffleChain T 0 (q + 1) (n + 1) h = CategoryTheory.CategoryStruct.comp (shuffleChain T 0 q n ⋯) (CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSimplex.obj { len := 0 }) (stdSimplex.δ 0)) T).f n) (stdSimplex.prodConeChain 0 (q + 1) T n))

The shuffle chain of Δ[0] ⊗ Δ[q + 1] is the cone on the shuffle chain of Δ[0] ⊗ Δ[q], pushed along the zeroth face of Δ[q + 1].

theorem SSet.shuffleChain_succ_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (p q n : ℕ) (h : p + 1 + (q + 1) = n + 1) : shuffleChain T (p + 1) (q + 1) (n + 1) h = CategoryTheory.CategoryStruct.comp (shuffleChain T p (q + 1) n ⋯) (CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight (stdSimplex.δ 0) (stdSimplex.obj { len := q + 1 })) T).f n) (stdSimplex.prodConeChain (p + 1) (q + 1) T n)) + (-1) ^ (p + 1) • CategoryTheory.CategoryStruct.comp (shuffleChain T (p + 1) q n ⋯) (CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSimplex.obj { len := p + 1 }) (stdSimplex.δ 0)) T).f n) (stdSimplex.prodConeChain (p + 1) (q + 1) T n))

The shuffle chain of Δ[p + 1] ⊗ Δ[q + 1] is the cone on the shuffle chain of Δ[p] ⊗ Δ[q + 1] pushed along the zeroth face of Δ[p + 1], plus (-1)^(p + 1) times the cone on the shuffle chain of Δ[p + 1] ⊗ Δ[q] pushed along the zeroth face of Δ[q + 1].

theorem SSet.shuffleChain_d_succ_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (p q n : ℕ) (h : p + 1 + (q + 1) = n + 1) : CategoryTheory.CategoryStruct.comp (shuffleChain T (p + 1) (q + 1) (n + 1) h) (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p + 1 }) (stdSimplex.obj { len := q + 1 })).chainComplex T).d (n + 1) n) = CategoryTheory.CategoryStruct.comp (shuffleChain T p (q + 1) n ⋯) (∑ j : Fin (p + 2), (-1) ^ ↑j • (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight (stdSimplex.δ j) (stdSimplex.obj { len := q + 1 })) T).f n) + (-1) ^ (p + 1) • CategoryTheory.CategoryStruct.comp (shuffleChain T (p + 1) q n ⋯) (∑ j : Fin (q + 2), (-1) ^ ↑j • (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSimplex.obj { len := p + 1 }) (stdSimplex.δ j)) T).f n)

The boundary of the shuffle chain of Δ[p + 1] ⊗ Δ[q + 1]: the alternating sum of its faces in the first factor plus (-1)^(p + 1) times the alternating sum of its faces in the second factor, each face being the image of a smaller shuffle chain under a face map.

theorem SSet.shuffleChain_d_succ_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (p n : ℕ) (h : p + 1 + 0 = n + 1) : CategoryTheory.CategoryStruct.comp (shuffleChain T (p + 1) 0 (n + 1) h) (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := p + 1 }) (stdSimplex.obj { len := 0 })).chainComplex T).d (n + 1) n) = CategoryTheory.CategoryStruct.comp (shuffleChain T p 0 n ⋯) (∑ j : Fin (p + 2), (-1) ^ ↑j • (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight (stdSimplex.δ j) (stdSimplex.obj { len := 0 })) T).f n)

The boundary of the shuffle chain of Δ[p + 1] ⊗ Δ[0]: the alternating sum of its faces in the first factor.

theorem SSet.shuffleChain_d_zero_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (T : C) (q n : ℕ) (h : 0 + (q + 1) = n + 1) : CategoryTheory.CategoryStruct.comp (shuffleChain T 0 (q + 1) (n + 1) h) (((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj { len := 0 }) (stdSimplex.obj { len := q + 1 })).chainComplex T).d (n + 1) n) = CategoryTheory.CategoryStruct.comp (shuffleChain T 0 q n ⋯) (∑ j : Fin (q + 2), (-1) ^ ↑j • (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSimplex.obj { len := 0 }) (stdSimplex.δ j)) T).f n)

The boundary of the shuffle chain of Δ[0] ⊗ Δ[q + 1]: the alternating sum of its faces in the second factor.

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

The shuffle map C(K; R) ⊗ C(L; S) ⟶ C(K × L; R ⊗ S) of Eilenberg and Mac Lane. It sends the summand of a p-simplex x of K and a q-simplex y of L to the image of the shuffle chain SSet.shuffleChain (R ⊗ S) p q (p + q) under the map Δ[p] ⊗ Δ[q] ⟶ K ⊗ L classifying (x, y) (SSet.ιChainComplex_tensorHom_ιChainComplex_shuffle_f). It is a morphism of chain complexes for the Koszul sign rule on the tensor product.

Equations

• K.shuffle L R S = { f := SSet.shuffleX✝ K L R S, comm' := ⋯ }

@[simp]

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

The shuffle map on the summand of a p-simplex x of K and a q-simplex y of L is the image of the shuffle chain of Δ[p] ⊗ Δ[q] under the map Δ[p] ⊗ Δ[q] ⟶ K ⊗ L classifying (x, y).

@[simp]

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

The shuffle map on the summand of a p-simplex x of K and a q-simplex y of L is the image of the shuffle chain of Δ[p] ⊗ Δ[q] under the map Δ[p] ⊗ Δ[q] ⟶ K ⊗ L classifying (x, y).

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

In degree zero, the shuffle map sends the summand of a pair of vertices (x, y) to the summand of the vertex (x, y) of K × L.

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

The shuffle map is natural in both simplicial sets.

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

The shuffle map is natural in both simplicial sets.

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

The shuffle map is natural in both coefficient objects.

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

The shuffle map is natural in both coefficient objects.