isZero₁_iff — Mathlib

English

A compact criterion says that T.isZero₁ is equivalent to the conjunction of the shifted morphism zeros mor1 and mor3 being zero, reflecting a global zero condition on the triangle.

Русский

Компактная характеристика: T.isZero1 равносильна сочетанию нулей сдвинутых морфизмов mor1 и mor3, что отражает глобальное нулевое условие треугольника.

LaTeX

$$$IsZero(T.obj_1) \\iff (T.mor_1 = 0 \\land T.mor_3 = 0)$$$

Lean4

theorem isZero₁_iff : IsZero T.obj₁ ↔ (T.mor₁ = 0 ∧ T.mor₃ = 0) :=
  by
  refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_
  dsimp
  simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]
  tauto

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