Chain homotopies of simplicial objects in a commutative square

A simplicial homotopy between morphisms of simplicial objects induces a chain homotopy between the induced morphisms of alternating face map complexes. This file records that the construction is compatible with a commutative square: two simplicial homotopies whose defining families of morphisms commute with a pair of morphisms of simplicial objects give chain homotopies whose components commute with the induced chain maps.

This is the form in which the construction is applied to a pair of simplicial sets, where the square is the inclusion of the subcomplex.

theorem CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy_hom_comm {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y X' Y' : SimplicialObject C} {f g : X ⟶ Y} {f' g' : X' ⟶ Y'} (H : Homotopy f g) (H' : Homotopy f' g') (u : X ⟶ X') (v : Y ⟶ Y') (hu : ∀ (n : ℕ) (i : Fin (n + 1)), CategoryStruct.comp (u.app (Opposite.op { len := n })) (H'.h i) = CategoryStruct.comp (H.h i) (v.app (Opposite.op { len := n + 1 }))) (p q : ℕ) : CategoryStruct.comp (((AlgebraicTopology.alternatingFaceMapComplex C).map u).f p) (H'.toChainHomotopy.hom p q) = CategoryStruct.comp (H.toChainHomotopy.hom p q) (((AlgebraicTopology.alternatingFaceMapComplex C).map v).f q)

Simplicial homotopies which are compatible with a commutative square of simplicial objects induce compatible chain homotopies on the alternating face map complexes.