English
If F commutes with shifts, there exists a natural isomorphism expressing the compatibility of F.mapTriangle with triangleOpEquivalence on C and D, i.e. an isomorphism between F.mapTriangle.op ⋯ and ⋯ (triangleOpEquivalence C).functor ⋅ F.op.mapTriangle.
Русский
Если F совместим со сдвигами, существует естественный изоморфизм, выражающий совместимость F.mapTriangle с треугольниковой эквивалентностью на C и D.
LaTeX
$$$F.mapTriangle.op \; \circ (\operatorname{triangleOpEquivalence} D).functor \cong (\operatorname{triangleOpEquivalence} C).functor \circ F.op.mapTriangle$$$
Lean4
/-- If `F : C ⥤ D` commutes with shifts, this expresses the compatibility of `F.mapTriangle`
with the equivalences `Pretriangulated.triangleOpEquivalence` on `C` and `D`.
-/
noncomputable def mapTriangleOpCompTriangleOpEquivalenceFunctor :
F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor ≅ (triangleOpEquivalence C).functor ⋙ F.op.mapTriangle :=
NatIso.ofComponents (fun T ↦ F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T.unop)
(by intros; ext <;> dsimp <;> simp only [comp_id, id_comp])
