isZero₃_of_isZero₁₂ — Mathlib

English

Let C be a category with a zero object and T a distinguished triangle in distTriang C. If T.obj1 and T.obj2 are zero objects, then T.obj3 is a zero object.

Русский

Пусть C — категория с нулевым объектом, и T — распознаваемый треугольник в distTriang C. Если объекты T.obj1 и T.obj2 нулевые, то и T.obj3 нулевой.

LaTeX

$$$(T \\in \\mathrm{distTriang} \\, C) \\land \\mathrm{IsZero}(T.obj_1) \\land \\mathrm{IsZero}(T.obj_2) \\Rightarrow \\mathrm{IsZero}(T.obj_3)$$$

Lean4

theorem isZero₃_of_isZero₁₂ (h₁ : IsZero T.obj₁) (h₂ : IsZero T.obj₂) : IsZero T.obj₃ :=
  isZero₂_of_isZero₁₃ _ (rot_of_distTriang _ hT) h₂
    (by
      dsimp
      simp only [IsZero.iff_id_eq_zero] at h₁ ⊢
      rw [← Functor.map_id, h₁, Functor.map_zero])

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