English
Let F: C → D commute with shifts. For X ∈ C^op and n ∈ ℤ, F.map ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop equals the corresponding expression in D as in the previous item but with inverse unit and shifted arguments.
Русский
Пусть F: C → D коммутирует со сдвигами. Для X ∈ C^op и n ∈ ℤ, F.map инверсной counit в X равен соответствующему выражению в D.
LaTeX
$$$F.map ((\operatorname{opShiftFunctorEquivalence} C n).counitIso.inv.app X).unop = ((\operatorname{opShiftFunctorEquivalence} D n).counitIso.inv.app (op (F.obj X.unop))).unop \circ (((F.commShiftIso n).hom.app X.unop).op⟦n⟧').unop \circ ((F.op.commShiftIso n).hom.app (op (X.unop⟦n⟧))).unop$$$
Lean4
/-- If `F : C ⥤ D` commutes with shifts, this expresses the compatibility of `F.mapTriangle`
with the equivalences `Pretriangulated.triangleOpEquivalence` on `C` and `D`.
-/
@[simps!]
noncomputable def mapTriangleOpCompTriangleOpEquivalenceFunctorApp (T : Triangle C) :
(triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T)) ≅
F.op.mapTriangle.obj ((triangleOpEquivalence C).functor.obj (op T)) :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
(by
dsimp
simp only [map_comp, shift_map_op, map_id, comp_id, op_comp, op_unop,
map_opShiftFunctorEquivalence_counitIso_inv_app_unop, opShiftFunctorEquivalence_inverse,
opShiftFunctorEquivalence_functor, Quiver.Hom.op_unop, assoc, id_comp])
