mor₁_eq_zero_iff_mono₂ — Mathlib

English

Characterizations of zero objects in the components of a distinguished triangle: obj1, obj2, obj3 are zero precisely when certain morphisms vanish or factorize, with equivalent descriptions via isZero conditions on the morphisms.

Русский

Характеризации нулевых объектов в компонентах отличимого треугольника: объект1, объект2, объект3 равны нулю тогда и только тогда, когда определённые морфизмы исчезают или факторизуются.

LaTeX

$$$\\text{IsZero}(T.obj_1) \\iff (T.mor_1 = 0 \\land T.mor_3 = 0)$, and analogous for 2 and 3 with suitable rotations$$

Lean4

theorem mor₁_eq_zero_iff_mono₂ : T.mor₁ = 0 ↔ Mono T.mor₂ :=
  by
  constructor
  · intro h
    rw [mono_iff_cancel_zero]
    intro X g hg
    obtain ⟨f, rfl⟩ := coyoneda_exact₂ T hT g hg
    rw [h, comp_zero]
  · intro
    rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]

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