English
Given two distinguished triangles T1, T2 in Opposite C and a commuting square of morphisms at the first two entries a, b, there exists a morphism c at the third entry completing the distinguished triangles, satisfying the compatibility with mor₂ and mor₃ up to rotation by shift functors.
Русский
Пусть существуют два выделенных треугольника T1, T2 в Opposite C и квадрат морфизмов, содержащий a, b, тогда существует морфизм c на третьем месте, завершающий пары треугольников и удовлетворяющий совместимости mor₂ и mor₃ до сдвига.
LaTeX
$$$\exists c:\, T_1.obj_3 \to T_2.obj_3,\; T_1.mor_2 \circ c = b \circ T_2.mor_2 \land \; T_1.mor_3 \circ a\langle 1 \rangle' = c \circ T_2.mor_3$$$
Lean4
/-- Isomorphism expressing a compatibility of the equivalence `triangleOpEquivalence C`
with the rotation of triangles. -/
noncomputable def rotateTriangleOpEquivalenceInverseObjRotateUnopIso (T : Triangle Cᵒᵖ) :
((triangleOpEquivalence C).inverse.obj T.rotate).unop.rotate ≅ ((triangleOpEquivalence C).inverse.obj T).unop :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop) (by simp)
(Quiver.Hom.op_inj (by simp)) (by simp)
