English
Let C be a triangulated category with zero object and shift. For any object property P and any distinguished triangle T whose third object lies in P, P holds for the first morphism of T after applying the W-construction.
Русский
Пусть C — треугольная категория с нулевым объектом и сдвигом. Пусть P — свойство объекта, и пусть T — дискриминированный треугольник с T.obj3 ∈ P. Тогда свойство P выполняется для mor1 треугольника T после применения преобразования trW.
LaTeX
$$$\\forall {\\mathcal C}\, [\\text{Category } \\mathcal C], [\\text{HasZeroObject } \\mathcal C], [\\text{HasShift } \\mathcal C \\mathbb{Z}], [\\text{Preadditive } \\mathcal C], (P : \\mathrm{ObjectProperty}\\, \\mathcal C) \\,\\to \\\\forall {T : \\mathrm{Triangle}\\, \\mathcal C}, T \\in \\mathrm{distTriang}\\, \\mathcal C \\to P(T.obj_3) \\to P\\,\\mathrm{trW}\\, T.mor_1.$$$
Lean4
theorem mk {T : Triangle C} (hT : T ∈ distTriang C) (h : P T.obj₃) : P.trW T.mor₁ :=
⟨_, _, _, hT, h⟩
