mapToComposableArrows_id — Mathlib

English

The induced map of composable arrows preserves identities: mapToComposableArrows(id_S) = id_{S^{comp}}.

Русский

Индуцированное отображение сохраняет тождественный морфизм: mapToComposableArrows(id_S) = id_{S^{comp}}.

LaTeX

$$$\operatorname{mapToComposableArrows}(\mathrm{id}_S) = \mathrm{id}_{S^{\mathrm{comp}}}$$$

Lean4

@[simp]
theorem mapToComposableArrows_id {S₁ : ShortComplex C} :
    (ShortComplex.mapToComposableArrows (𝟙 S₁)) = 𝟙 S₁.toComposableArrows := by cat_disch

Похожие утверждения