English
The inverse functor from the Opposite side provides a correspondence between triangles in Cᵒᵖ and triangles in C, again up to natural isomorphism.
Русский
Обратный функтор между сторонами противоположностей устанавливает корреспонденцию треугольников между Cᵒᵖ и C, опять же через естественные изоморфизмы.
LaTeX
$$((\\triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C$$
Lean4
/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `Cᵒᵖ` to the triangle
`Z.unop ⟶ Y.unop ⟶ X.unop ⟶ Z.unop⟦1⟧` in `C` (without introducing signs). -/
@[simps]
noncomputable def inverse : Triangle Cᵒᵖ ⥤ (Triangle C)ᵒᵖ
where
obj
T :=
Opposite.op
(Triangle.mk T.mor₂.unop T.mor₁.unop
(((opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ≫ T.mor₃.unop⟦(1 : ℤ)⟧'))
map {T₁ T₂}
φ :=
Quiver.Hom.op
{ hom₁ := φ.hom₃.unop
hom₂ := φ.hom₂.unop
hom₃ := φ.hom₁.unop
comm₁ := Quiver.Hom.op_inj φ.comm₂.symm
comm₂ := Quiver.Hom.op_inj φ.comm₁.symm
comm₃ :=
Quiver.Hom.op_inj
(by
dsimp
rw [assoc, ← opShiftFunctorEquivalence_unitIso_inv_naturality, ← op_comp_assoc, ← Functor.map_comp, ←
unop_comp, ← φ.comm₃, unop_comp, Functor.map_comp, op_comp, assoc]) }
