triangleOpEquivalence — Mathlib

English

The functor sending a distinguished triangle in C to its opposite triangle in Cᵒᵖ is an equivalence, preserving the distinguished structure up to isomorphism.

Русский

Функтор, отправляющий выделенный треугольник в C в противоположный треугольник в Cᵒᵖ, является эквивалентностью, сохраняющей выделенную структуру до изоморфизма.

LaTeX

$$$\\text{triangleOpEquivalence}: (Triangle\\; C)^{op} \\simeq Triangle\\; (C^{op})$$$

Lean4

/-- An anti-equivalence between the categories of triangles in `C` and in `Cᵒᵖ`.
A triangle in `Cᵒᵖ` shall be distinguished iff it correspond to a distinguished
triangle in `C` via this equivalence. -/
@[simps]
noncomputable def triangleOpEquivalence : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ
    where
  functor := TriangleOpEquivalence.functor C
  inverse := TriangleOpEquivalence.inverse C
  unitIso := TriangleOpEquivalence.unitIso C
  counitIso := TriangleOpEquivalence.counitIso C

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