English
The associativity constraint for composition in the SimplicialThickening framework holds: the two ways of composing three morphisms are equal.
Русский
Свойство ассоциативности композиции в рамках SimplicialThickening: оба способа композиции трёх морфизмов совпадают.
LaTeX
$$$$ (\alpha_{\mathrm{Hom}(i j),\mathrm{Hom}(j k),\mathrm{Hom}(k l)})^{-1} \;\circ (\mathrm{comp}_{i j k} \triangleright \mathrm{Hom}(k l)) \circ \mathrm{comp}_{i k l} \\ = \; (\mathrm{Hom}(i j) \triangleright \mathrm{comp}_{j k l}) \circ \mathrm{comp}_{i j l} $$$$
Lean4
/-- Composition of morphisms in `SimplicialThickening J`, as a functor `(i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k)`
-/
@[simps]
def compFunctor {J : Type*} [LinearOrder J] (i j k : SimplicialThickening J) : (i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k)
where
obj x := x.1 ≫ x.2
map f := ⟨⟨Set.union_subset_union f.1.1.1 f.2.1.1⟩⟩
