functor_isTriangulated_op — Mathlib

English

The opposite-level square relating mapTriangle and triangleOpEquivalence is coherent, yielding a commutative square up to isomorphism.

Русский

Противоположный квадрат между mapTriangle и triangleOpEquivalence совместим и приводится к согласованию посредством изоморфизма.

LaTeX

$$$F.op.mapTriangle \circ (triangleOpEquivalence C).inverse \cong (triangleOpEquivalence D).inverse \circ F.mapTriangle.op$$$

Lean4

/-- If `F` is triangulated, so is `F.op`.
-/
scoped instance functor_isTriangulated_op [F.IsTriangulated] : F.op.IsTriangulated where
  map_distinguished T
    dT := by
    rw [mem_distTriang_op_iff]
    exact
      Pretriangulated.isomorphic_distinguished _ ((F.map_distinguished _ (unop_distinguished _ dT))) _
        (((opMapTriangleCompTriangleOpEquivalenceInverse F).symm.app T).unop)

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