isZero₁_iff_isIso₂ — Mathlib

English

For a distinguished triangle T, the property IsZero T.obj1 is equivalent to IsIso T.mor2.

Русский

Для распознаваемого треугольника T свойство IsZero T.obj1 эквивалентно тому, что mor2 является изоморфизмом.

LaTeX

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

Lean4

theorem isZero₁_iff_isIso₂ : IsZero T.obj₁ ↔ IsIso T.mor₂ :=
  by
  rw [T.isZero₁_iff hT]
  constructor
  · intro ⟨h₁, h₃⟩
    have := T.epi₂ hT h₃
    obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, zero_comp])
    exact ⟨f, hf.symm, by rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]⟩
  · intro
    rw [T.mor₁_eq_zero_iff_mono₂ hT, T.mor₃_eq_zero_iff_epi₂ hT]
    constructor <;> infer_instance

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