English
There is a canonical isomorphism between the contractible triangle in C^op and the corresponding triangle under the opposite of the contractible triangle in C.
Русский
Существует канонический изоморфизм между контрактным треугольником в C^op и соответствующим треугольником под противоположной конструкцией контрактного треугольника в C.
LaTeX
$$$\text{contractibleTriangle } X \cong (\text{triangleOpEquivalence } C)^{-1}(\text{contractibleTriangle } X^{unop})$$$
Lean4
/-- Up to rotation, the contractible triangle `X ⟶ X ⟶ 0 ⟶ X⟦1⟧` for `X : Cᵒᵖ` corresponds
to the contractible triangle for `X.unop` in `C`. -/
@[simps!]
noncomputable def contractibleTriangleIso (X : Cᵒᵖ) :
contractibleTriangle X ≅
(triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle X.unop).invRotate) :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
(IsZero.iso (isZero_zero _)
(by
dsimp
rw [IsZero.iff_id_eq_zero]
change (𝟙 ((0 : C)⟦(-1 : ℤ)⟧)).op = 0
rw [← Functor.map_id, id_zero, Functor.map_zero, op_zero]))
(by simp) (by simp) (by simp)
