English
The triangle opposite construction defines a functor from triangles in C to triangles in Cᵒᵖ, reversing arrows, and preserving the triangle structure up to canonical isomorphisms.
Русский
Операция противоположного треугольника задаёт функтор от треугольников в C к треугольникам в Cᵒᵖ, обращая стрелки и сохраняет треугольную структуру до канонических изоморфизмов.
LaTeX
$$$\\text{TriangleOpEquivalence.functor}: (Triangle C)^{op} \\to Triangle (C^{op})$$$
Lean4
/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `C` to the triangle
`op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧` in `Cᵒᵖ` (without introducing signs). -/
@[simps]
noncomputable def functor : (Triangle C)ᵒᵖ ⥤ Triangle Cᵒᵖ
where
obj
T :=
Triangle.mk T.unop.mor₂.op T.unop.mor₁.op
((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op T.unop.obj₁) ≫ T.unop.mor₃.op⟦(1 : ℤ)⟧')
map {T₁ T₂}
φ :=
{ hom₁ := φ.unop.hom₃.op
hom₂ := φ.unop.hom₂.op
hom₃ := φ.unop.hom₁.op
comm₁ := Quiver.Hom.unop_inj φ.unop.comm₂.symm
comm₂ := Quiver.Hom.unop_inj φ.unop.comm₁.symm
comm₃ := by
dsimp
rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp,
opShiftFunctorEquivalence_counitIso_inv_naturality_assoc]
rfl }
