isZero₂_iff_isIso₃

Mathlib.CategoryTheory.Triangulated.Pretriangulated

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃

English

For a distinguished triangle T, IsZero T.obj2 is equivalent to IsIso T.mor3.

Русский

Для распознаваемого треугольника T: IsZero T.obj2 эквивалентно IsIso T.mor3.

LaTeX

$$$(T \\in \\mathrm{distTriang} \\, C) \\Rightarrow (\\mathrm{IsZero}(T.obj_2) \\leftrightarrow \\mathrm{IsIso}(T.mor_3))$$$

Lean4

theorem isZero₂_iff_isIso₃ : IsZero T.obj₂ ↔ IsIso T.mor₃ :=
  isZero₁_iff_isIso₂ _ (rot_of_distTriang _ hT)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru