English
Within a distinguished triangle, the Yoneda-type exactness yields that certain morphisms into the middle object factor through the adjacent morphism; concretely, if f lands in the middle object and certain shifted composites vanish, then f factors through mor2 via mor1.
Русский
В отличимом треугольнике Йонеда-подобная точность дает факторизацию некоторых морфизмов в середину через смежное отображение; если $f$ имеет значение в середине и определённые сдвинутые композиции равны нулю, то $f$ факторизуется через $mor_2$ через $mor_1$.
LaTeX
$$$\\forall X$, $f: X \\to T_{2}$, $(f \\circ T_{m,2}) = 0 \\Rightarrow \\ exists\\ g: X \\to T_{1},\\ f = g \\circ T_{m,1}$$$
Lean4
theorem mor₃_eq_zero_iff_epi₂ : T.mor₃ = 0 ↔ Epi T.mor₂ :=
by
constructor
· intro h
rw [epi_iff_cancel_zero]
intro X g hg
obtain ⟨f, rfl⟩ := yoneda_exact₃ T hT g hg
rw [h, zero_comp]
· intro
rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, comp_zero]
