isZero₁_of_isIso₂

Mathlib.CategoryTheory.Triangulated.Pretriangulated

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂

English

If mor3 is an isomorphism, then T.obj2 is zero.

Русский

Если mor3 — изоморфизм, то T.obj2 нулевой объект.

LaTeX

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

Lean4

theorem isZero₁_of_isIso₂ (h : IsIso T.mor₂) : IsZero T.obj₁ :=
  (T.isZero₁_iff_isIso₂ hT).2 h

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

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

Разделы

Аффилиация

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