English
The functor composableArrowsFunctor maps SnakeInput C to the diagram with five composable arrows, encoding the data (L0.X1 → L0.X2 → L0.X3 → L3.X1 → L3.X2 → L3.X3) together with the associating morphisms and naturality data.
Русский
Функтор composableArrowsFunctor отображает SnakeInput C в диаграмму с пятью последовательными стрелами, задавая данные (L0.X1 → L0.X2 → L0.X3 → L3.X1 → L3.X2 → L3.X3) вместе с соответствующими отображениями и натуральностными данными.
LaTeX
$$$$ \text{composableArrowsFunctor} : \text{SnakeInput } C \to \text{ComposableArrows } C\ 5 $$$$
Lean4
/-- The functor which maps `S : SnakeInput C` to the diagram
`S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃`. -/
@[simps]
noncomputable def composableArrowsFunctor : SnakeInput C ⥤ ComposableArrows C 5
where
obj S := S.composableArrows
map
f :=
ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃ f.f₀.comm₁₂.symm f.f₀.comm₂₃.symm
(naturality_δ f) f.f₃.comm₁₂.symm f.f₃.comm₂₃.symm
