English
The trW predicate assigns to each morphism a witness cone through a distinguished triangle whose apex satisfies the property P. It is used to define a class of morphisms suitable for localization.
Русский
Предикат trW назначает каждому морфизму свидетельский конус через выделенный треугольник, вершина которого удовлетворяет свойству P; его используют для локализации.
LaTeX
$$$\\text{trW}(f) := \\exists Z,g,h,\\; \\triangle(f,g,h) \\in distTriang(C)$ и $P Z$$$
Lean4
/-- Given `P : ObjectProperty C` with `C` a pretriangulated category, this is the class
of morphisms whose cone satisfies `P`. (The name `trW` contains the prefix `tr`
for "triangulated", and `W` is a letter that is often used to refer to classes of
morphisms with respect to which we may consider the localized category.) -/
def trW : MorphismProperty C := fun X Y f =>
∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧) (_ : Triangle.mk f g h ∈ distTriang C), P Z
