Coefficient pairings on simplicial chains

Let C be a preadditive monoidal category with w-small coproducts, and let M be an object of C such that M ⊗ - preserves w-small coproducts (for instance, any object of a closed monoidal category such as ModuleCat k). The simplicial chains Cₙ(X; S) of a simplicial set X are the coproduct of one copy of S for each n-simplex, so M ⊗ Cₙ(X; S) is the coproduct of one copy of M ⊗ S for each n-simplex. A pairing μ : M ⊗ S ⟶ P of coefficient objects therefore induces, simplex by simplex, a chain map X.chainComplexPairing μ from the complex M ⊗ C(X; S) to C(X; P): it is the identification M ⊗ C(X; S) ≅ C(X; M ⊗ S) of Mathlib's SSet.chainComplexFunctorObjCompMapIso (for the coproduct-preserving functor M ⊗ -), followed by the chain map induced by μ. It is natural in X and in the coefficient objects.

This is how the coefficients of a cochain act on chains in the cap product: capping with a cochain φ : Cₚ(X; R) ⟶ M produces an element of M ⊗ C_q(X; S), which the pairing turns into a chain with coefficients in P.

In the same way, when tensoring on either side preserves w-small coproducts, the tensor product Cₚ(K; R) ⊗ C_q(L; S) of chain groups of two simplicial sets is the coproduct of one copy of R ⊗ S for each pair of a p-simplex of K and a q-simplex of L, which describes morphisms out of tensor products of simplicial chains, such as the shuffle map.

Main definitions and results

• SSet.ιChainComplex_chainComplexFunctorObjCompMapIso_inv_app_f: the inverse of Mathlib's identification F(C(X; R)) ≅ C(X; F(R)) on the summand of a simplex.
• SSet.chainComplexPairing: the chain map M ⊗ C(X; S) ⟶ C(X; P) induced by μ.
• SSet.whiskerLeft_ιChainComplex_chainComplexPairing_f: its value on the summand of a simplex.
• SSet.chainComplexPairing_naturality: it is natural in the simplicial set.
• SSet.chainComplexPairing_comp_chainComplexFunctor_map_app, SSet.whiskerLeft_chainComplexFunctor_map_app_comp_chainComplexPairing and SSet.whiskerRight_comp_chainComplexPairing: it is natural in the coefficient objects.
• SSet.tensorChainComplexXDesc and SSet.tensorChainComplexX_hom_ext: morphisms out of the tensor product Cₚ(K; R) ⊗ C_q(L; S) of two chain groups are given, and determined, by their values on the summands R ⊗ S of pairs of simplices.

@[simp]

theorem SSet.ιChainComplex_chainComplexFunctorObjCompMapIso_inv_app_f {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoproducts D] (X : SSet) (F : CategoryTheory.Functor C D) [F.Additive] [∀ (T : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete T) F] (R : C) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (((chainComplexFunctorObjCompMapIso F R).inv.app X).f n) = F.map (X.ιChainComplex x)

The inverse of the identification F(C(X; R)) ≅ C(X; F(R)) of SSet.chainComplexFunctorObjCompMapIso, for a coproduct-preserving functor F, sends the summand F(R) of a simplex x to the image under F of the summand R of x. Morphisms out of F(Cₙ(X; R)) are therefore determined on these images.

@[simp]

theorem SSet.ιChainComplex_chainComplexFunctorObjCompMapIso_inv_app_f_assoc {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoproducts D] (X : SSet) (F : CategoryTheory.Functor C D) [F.Additive] [∀ (T : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete T) F] (R : C) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : D} (h : ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (((chainComplexFunctor C).obj R).obj X)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (CategoryTheory.CategoryStruct.comp (((chainComplexFunctorObjCompMapIso F R).inv.app X).f n) h) = CategoryTheory.CategoryStruct.comp (F.map (X.ιChainComplex x)) h

The inverse of the identification F(C(X; R)) ≅ C(X; F(R)) of SSet.chainComplexFunctorObjCompMapIso, for a coproduct-preserving functor F, sends the summand F(R) of a simplex x to the image under F of the summand R of x. Morphisms out of F(Cₙ(X; R)) are therefore determined on these images.

noncomputable def SSet.tensorChainComplexXDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] {K L : SSet} {R S A : C} {p q : ℕ} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft R)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (φ : K.obj (Opposite.op { len := p }) → L.obj (Opposite.op { len := q }) → (CategoryTheory.MonoidalCategoryStruct.tensorObj R S ⟶ A)) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((K.chainComplex R).X p) ((L.chainComplex S).X q) ⟶ A

The morphism out of the tensor product Cₚ(K; R) ⊗ C_q(L; S) of two simplicial chain groups given by a morphism φ x y : R ⊗ S ⟶ A for each p-simplex x of K and q-simplex y of L (SSet.ιChainComplex_tensorHom_ιChainComplex_tensorChainComplexXDesc). When tensoring preserves coproducts, Cₚ(K; R) ⊗ C_q(L; S) is the coproduct of one copy of R ⊗ S for each such pair.

Equations

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

@[simp]

theorem SSet.ιChainComplex_tensorHom_ιChainComplex_tensorChainComplexXDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] {K L : SSet} {R S A : C} {p q : ℕ} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft R)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (φ : K.obj (Opposite.op { len := p }) → L.obj (Opposite.op { len := q }) → (CategoryTheory.MonoidalCategoryStruct.tensorObj R S ⟶ A)) (x : K.obj (Opposite.op { len := p })) (y : L.obj (Opposite.op { len := q })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (K.ιChainComplex x) (L.ιChainComplex y)) (tensorChainComplexXDesc φ) = φ x y

The morphism SSet.tensorChainComplexXDesc φ on the summand of a pair of simplices (x, y) is φ x y.

@[simp]

theorem SSet.ιChainComplex_tensorHom_ιChainComplex_tensorChainComplexXDesc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] {K L : SSet} {R S A : C} {p q : ℕ} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft R)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (φ : K.obj (Opposite.op { len := p }) → L.obj (Opposite.op { len := q }) → (CategoryTheory.MonoidalCategoryStruct.tensorObj R S ⟶ A)) (x : K.obj (Opposite.op { len := p })) (y : L.obj (Opposite.op { len := q })) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (K.ιChainComplex x) (L.ιChainComplex y)) (CategoryTheory.CategoryStruct.comp (tensorChainComplexXDesc φ) h) = CategoryTheory.CategoryStruct.comp (φ x y) h

The morphism SSet.tensorChainComplexXDesc φ on the summand of a pair of simplices (x, y) is φ x y.

theorem SSet.tensorChainComplexX_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] {K L : SSet} {R S A : C} {p q : ℕ} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft R)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj ((K.chainComplex R).X p) ((L.chainComplex S).X q) ⟶ A} (h : ∀ (x : K.obj (Opposite.op { len := p })) (y : L.obj (Opposite.op { len := q })), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (K.ιChainComplex x) (L.ιChainComplex y)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (K.ιChainComplex x) (L.ιChainComplex y)) g) : f = g

Morphisms out of Cₚ(K; R) ⊗ C_q(L; S) are determined on the summands of pairs of simplices.

noncomputable def SSet.chainComplexPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj (X.chainComplex S) ⟶ X.chainComplex P

The chain map induced by a coefficient pairing μ : M ⊗ S ⟶ P: the chain map M ⊗ C(X; S) ⟶ C(X; P) which sends the summand M ⊗ S of a simplex x to the summand P of x through μ (SSet.whiskerLeft_ιChainComplex_chainComplexPairing_f). It is the identification M ⊗ C(X; S) ≅ C(X; M ⊗ S) followed by the chain map induced by μ.

Equations

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

@[simp]

theorem SSet.whiskerLeft_ιChainComplex_chainComplexPairing_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) {n : ℕ} (x : X.obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (X.ιChainComplex x)) ((X.chainComplexPairing μ).f n) = CategoryTheory.CategoryStruct.comp μ (X.ιChainComplex x)

The chain map induced by a coefficient pairing μ sends the summand M ⊗ S of a simplex x to the summand P of x through μ.

@[simp]

theorem SSet.whiskerLeft_ιChainComplex_chainComplexPairing_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) {n : ℕ} (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (X.chainComplex P).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (X.ιChainComplex x)) (CategoryTheory.CategoryStruct.comp ((X.chainComplexPairing μ).f n) h) = CategoryTheory.CategoryStruct.comp μ (CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) h)

The chain map induced by a coefficient pairing μ sends the summand M ⊗ S of a simplex x to the summand P of x through μ.

theorem SSet.chainComplexPairing_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] {X Y : SSet} (f : X ⟶ Y) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map (chainComplexMap f S)) (Y.chainComplexPairing μ) = CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ) (chainComplexMap f P)

The chain map induced by a coefficient pairing is natural in the simplicial set.

theorem SSet.chainComplexPairing_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] {X Y : SSet} (f : X ⟶ Y) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : Y.chainComplex P ⟶ Z) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map (chainComplexMap f S)) (CategoryTheory.CategoryStruct.comp (Y.chainComplexPairing μ) h) = CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ) (CategoryTheory.CategoryStruct.comp (chainComplexMap f P) h)

The chain map induced by a coefficient pairing is natural in the simplicial set.

@[simp]

theorem SSet.chainComplexPairing_comp_chainComplexFunctor_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) {P' : C} (g : P ⟶ P') : CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ) (((chainComplexFunctor C).map g).app X) = X.chainComplexPairing (CategoryTheory.CategoryStruct.comp μ g)

Pushing the chain map induced by a coefficient pairing μ forward along a coefficient morphism g : P ⟶ P' is the chain map induced by the pairing μ ≫ g.

@[simp]

theorem SSet.chainComplexPairing_comp_chainComplexFunctor_map_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) {P' : C} (g : P ⟶ P') {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : ((chainComplexFunctor C).obj P').obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ) (CategoryTheory.CategoryStruct.comp (((chainComplexFunctor C).map g).app X) h) = CategoryTheory.CategoryStruct.comp (X.chainComplexPairing (CategoryTheory.CategoryStruct.comp μ g)) h

Pushing the chain map induced by a coefficient pairing μ forward along a coefficient morphism g : P ⟶ P' is the chain map induced by the pairing μ ≫ g.

@[simp]

theorem SSet.whiskerLeft_chainComplexFunctor_map_app_comp_chainComplexPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) {S' : C} (g : S ⟶ S') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M S' ⟶ P) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map (((chainComplexFunctor C).map g).app X)) (X.chainComplexPairing μ') = X.chainComplexPairing (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g) μ')

Precomposing the chain map induced by a coefficient pairing μ' with the chain map induced by a coefficient morphism g : S ⟶ S' is the chain map induced by the pairing (M ◁ g) ≫ μ'.

@[simp]

theorem SSet.whiskerLeft_chainComplexFunctor_map_app_comp_chainComplexPairing_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) {S' : C} (g : S ⟶ S') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M S' ⟶ P) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : X.chainComplex P ⟶ Z) : CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map (((chainComplexFunctor C).map g).app X)) (CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ') h) = CategoryTheory.CategoryStruct.comp (X.chainComplexPairing (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g) μ')) h

Precomposing the chain map induced by a coefficient pairing μ' with the chain map induced by a coefficient morphism g : S ⟶ S' is the chain map induced by the pairing (M ◁ g) ≫ μ'.

@[simp]

theorem SSet.whiskerRight_comp_chainComplexPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) {M' : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M')] (g : M ⟶ M') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M' S ⟶ P) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex ((CategoryTheory.MonoidalCategory.tensoringLeft C).map g) (ComplexShape.down ℕ)).app (X.chainComplex S)) (X.chainComplexPairing μ') = X.chainComplexPairing (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g S) μ')

Precomposing the chain map induced by a coefficient pairing μ' with the chain map g ▷ C(X; S) : M ⊗ C(X; S) ⟶ M' ⊗ C(X; S) induced by a coefficient morphism g : M ⟶ M' is the chain map induced by the pairing (g ▷ S) ≫ μ'.

@[simp]

theorem SSet.whiskerRight_comp_chainComplexPairing_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {M S P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : SSet) {M' : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M')] (g : M ⟶ M') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M' S ⟶ P) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : X.chainComplex P ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex ((CategoryTheory.MonoidalCategory.tensoringLeft C).map g) (ComplexShape.down ℕ)).app (X.chainComplex S)) (CategoryTheory.CategoryStruct.comp (X.chainComplexPairing μ') h) = CategoryTheory.CategoryStruct.comp (X.chainComplexPairing (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g S) μ')) h

Precomposing the chain map induced by a coefficient pairing μ' with the chain map g ▷ C(X; S) : M ⊗ C(X; S) ⟶ M' ⊗ C(X; S) induced by a coefficient morphism g : M ⟶ M' is the chain map induced by the pairing (g ▷ S) ≫ μ'.