isZero₃_iff_isIso₁ — Mathlib

English

For a distinguished triangle T, IsZero T.obj3 is equivalent to IsIso T.mor1.

Русский

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

LaTeX

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

Lean4

theorem isZero₃_iff_isIso₁ : IsZero T.obj₃ ↔ IsIso T.mor₁ :=
  by
  refine Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (inv_rot_of_distTriang _ hT))
  dsimp
  simp only [IsZero.iff_id_eq_zero, ← Functor.map_id, Functor.map_eq_zero_iff]

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