English
A functor F is triangulated if and only if its opposite F.op is triangulated.
Русский
Функтор F треугольный тогда и только тогда, когда его противоположность F.op треугольна.
LaTeX
$$$F.op.IsTriangulated \iff F.IsTriangulated$$$
Lean4
/-- If `F.op` is triangulated, so is `F`.
-/
theorem isTriangulated_of_op [F.op.IsTriangulated] : F.IsTriangulated where
map_distinguished T
dT :=
by
have := distinguished_iff_of_iso ((triangleOpEquivalence D).unitIso.app (Opposite.op (F.mapTriangle.obj T))).unop
rw [Functor.id_obj, Opposite.unop_op (F.mapTriangle.obj T)] at this
rw [← this, Functor.comp_obj, ← mem_distTriang_op_iff, ← Functor.op_obj, ← Functor.comp_obj,
distinguished_iff_of_iso ((mapTriangleOpCompTriangleOpEquivalenceFunctor F).app (Opposite.op T))]
apply F.op.map_distinguished
have := distinguished_iff_of_iso ((triangleOpEquivalence C).unitIso.app (Opposite.op T)).unop
rw [Functor.id_obj, Opposite.unop_op T] at this
rw [← this, Functor.comp_obj, ← mem_distTriang_op_iff] at dT
exact dT
