exact_iff_exact_toComposableArrows

English

For a ShortComplex S, S.Exact is equivalent to S.toComposableArrows.Exact.

Русский

Для краткого комплекса S условие точности эквивалентно точности S.toComposableArrows.

LaTeX

$$$S \text{ is a ShortComplex } \Rightarrow (S.\mathrm{Exact} \iff S^{\mathrm{to\,comp}}.\mathrm{Exact})$$$

Lean4

theorem _root_.CategoryTheory.ShortComplex.exact_iff_exact_toComposableArrows (S : ShortComplex C) :
    S.Exact ↔ S.toComposableArrows.Exact :=
  (S.toComposableArrows.exact₂_iff S.isComplex_toComposableArrows).symm

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