Homotopies of morphisms of pairs of simplicial sets

A homotopy between morphisms of a pair of simplicial sets consists of a homotopy on the subcomplexes and a homotopy on the total complexes which agree on the subcomplexes, that is, SSetPair.Homotopy. This is the simplicial analogue of TopPair.Homotopy in Mathlib/Topology/Category/TopPair.lean (J. Scharmberg), with the same two homotopies and the same whiskered commuting square.

The file also records what such a commuting square gives on the combinatorial homotopies that SSet.Homotopy.toSimplicialObjectHomotopy extracts: the two families of morphisms Xₙ ⟶ Y'ₙ₊₁ commute with the morphisms of the square. That compatibility is what makes the chain homotopies of the absolute case descend to relative chains.

theorem SSet.Homotopy.toSimplicialObjectHomotopy_h_comm {X Y X' Y' : SSet} {f g : X ⟶ Y} {f' g' : X' ⟶ Y'} {u : X ⟶ X'} {v : Y ⟶ Y'} (H : Homotopy f g) (H' : Homotopy f' g') (hu : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (stdSimplex.obj { len := 1 })) H'.h = CategoryTheory.CategoryStruct.comp H.h v) (n : ℕ) (i : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (u.app (Opposite.op { len := n })) (H'.toSimplicialObjectHomotopy.h i) = CategoryTheory.CategoryStruct.comp (H.toSimplicialObjectHomotopy.h i) (v.app (Opposite.op { len := n + 1 }))

Simplicial homotopies which fit into a commutative square induce compatible families of morphisms Xₙ ⟶ Y'ₙ₊₁.

structure SSetPair.Homotopy {P P' : SSetPair} (f g : P ⟶ P') : Type w

A homotopy between morphisms of pairs of simplicial sets consists of a homotopy on the subcomplexes and a homotopy on the total complexes which agree on the subcomplexes.

• left : SSet.Homotopy f.left g.left

  The homotopy on the subcomplexes.

• right : SSet.Homotopy f.right g.right

  The homotopy on the total complexes.

• w : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.hom (SSet.stdSimplex.obj { len := 1 })) self.right.h = CategoryTheory.CategoryStruct.comp self.left.h P'.hom

  The two homotopies agree on the subcomplexes.

theorem SSetPair.Homotopy.ext_iff {P P' : SSetPair} {f g : P ⟶ P'} {x y : Homotopy f g} : x = y ↔ x.left = y.left ∧ x.right = y.right

theorem SSetPair.Homotopy.ext {P P' : SSetPair} {f g : P ⟶ P'} {x y : Homotopy f g} (left : x.left = y.left) (right : x.right = y.right) : x = y