isZero₂_of_isIso₃ — Mathlib

English

Let φ: T ⟶ T' be a morphism of distinguished triangles with φ.hom1 and φ.hom3 isomorphisms. Then φ.hom2 is an isomorphism.

Русский

Пусть φ: T ⟶ T' — морфизм распознаваемых треугольников, и φ.hom1, φ.hom3 — изоморфизмы. Тогда φ.hom2 — изоморфизм.

LaTeX

$$$(T \\in \\mathrm{distTriang} \\, C) \\land (T' \\in \\mathrm{distTriang} \\, C) \Rightarrow \\Big( \\mathrm{IsIso}(\\varphi.hom_1) \\land \\mathrm{IsIso}(\\varphi.hom_3) \\Rightarrow \\mathrm{IsIso}(\\varphi.hom_2) \\Big)$$$

Lean4

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

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