English
Let S1 and S2 be short complexes in a category with zero morphisms, and let φ: S1 → S2 be a morphism of short complexes. Then φ induces a morphism between the associated composable-arrows objects, determined by the data φ.τ1, φ.τ2, φ.τ3 and the inverse of the compatibility data φ.comm12 and φ.comm23.
Русский
Пусть S1 и S2 — краткие комплексы в категории с нулевыми морфизмами, и φ: S1 → S2 — морфизм кратких комплексов. Тогда φ индуцирует морфизм между соответствующими объектами композиционных стрелок, задаваемый данными φ.τ1, φ.τ2, φ.τ3 и обратными compatibility-данными φ.comm12⁻¹, φ.comm23⁻¹.
LaTeX
$$$\operatorname{mapToComposableArrows}(\varphi): S_1^{\mathrm{comp}} \to S_2^{\mathrm{comp}}, \quad \operatorname{mapToComposableArrows}(\varphi) = (\varphi_1,\varphi_2,\varphi_3,(\varphi_{12})^{-1},(\varphi_{23})^{-1}).$$$
Lean4
/-- A map of short complexes induces a map of composable arrows with the same data. -/
def mapToComposableArrows {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : S₁.toComposableArrows ⟶ S₂.toComposableArrows :=
ComposableArrows.homMk₂ φ.τ₁ φ.τ₂ φ.τ₃ φ.comm₁₂.symm φ.comm₂₃.symm
