English
An instance asserting the coherence of the opposite-oriented triangle structure with the triangle equivalences is available.
Русский
Доступен экземпляр когерентности противоположной структуры треугольника с эквивалентностями треугольника.
LaTeX
$$$instCatCommSqOppositeTriangleOpEquivalence$$$
Lean4
/-- The pretriangulated structure on the opposite category of
a pretriangulated category. It is a scoped instance, so that we need to
`open CategoryTheory.Pretriangulated.Opposite` in order to be able
to use it: the reason is that it relies on the definition of the shift
on the opposite category `Cᵒᵖ`, for which it is unclear whether it should
be a global instance or not. -/
noncomputable scoped instance : Pretriangulated Cᵒᵖ
where
distinguishedTriangles := distinguishedTriangles C
isomorphic_distinguished := isomorphic_distinguished
contractible_distinguished := contractible_distinguished
distinguished_cocone_triangle := distinguished_cocone_triangle
rotate_distinguished_triangle := rotate_distinguished_triangle
complete_distinguished_triangle_morphism := complete_distinguished_triangle_morphism
