opMapTriangleCompTriangleOpEquivalenceInverse

English

Compatibility of mapTriangle with triangleOpEquivalence on opposite categories; the formula mirrors the earlier op-map-alt statements.

Русский

Совместимость отображения mapTriangle с эквивалентностью треугольника на противоположной категории.

LaTeX

$$$F \;\text{mapTriangle} \; op ⋅ (triangleOpEquivalence D)^{-1} = (triangleOpEquivalence C)^{-1} ⋅ F.mapTriangle.op$$$

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 opMapTriangleCompTriangleOpEquivalenceInverse :
    F.op.mapTriangle ⋙ (triangleOpEquivalence D).inverse ≅ (triangleOpEquivalence C).inverse ⋙ F.mapTriangle.op :=
  CatCommSq.iso (F.op.mapTriangle) (triangleOpEquivalence C).inverse (triangleOpEquivalence D).inverse F.mapTriangle.op

Похожие утверждения