English
Let F: C → D commute with shifts. For X ∈ C^op and n ∈ ℤ, F.map of the counit at X under opShiftFunctorEquivalence equals the composite: (op (F.obj X.unop)).unop ≫ (((F.commShiftIso n).inv.app X.unop).op⟦n⟧').unop ≫ (F.op.commShiftIso n).hom.app (op (X.unop⟦n⟧)).unop.
Русский
Пусть F: C → D коммутирует сдвиги. Для X ∈ C^op и n ∈ ℤ, отображение F по counit в X через opShiftFunctorEquivalence равно композиции: (op (F.obj X.unop)).unop ≫ (((F.commShiftIso n).inv.app X.unop).op⟦n⟧').unop ≫ (F.op.commShiftIso n).hom.app (op (X.unop⟦n⟧)).unop.
LaTeX
$$$F\map ((\operatorname{opShiftFunctorEquivalence} C \; n).counitIso.hom.app X) .unop = ((\operatorname{opShiftFunctorEquivalence} D \; n).counitIso.hom.app (op (F.obj X.unop))).unop \;\circ\; (((F.commShiftIso n).inv.app X.unop).op\langle n \rangle').unop \;\circ\; (F.op.commShiftIso n).hom.app (op (X.unop\langle n \rangle)).unop$$
Lean4
@[reassoc]
theorem map_opShiftFunctorEquivalence_counitIso_hom_app_unop (X : Cᵒᵖ) (n : ℤ) :
F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop =
((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj X.unop))).unop ≫
(((F.commShiftIso n).inv.app X.unop).op⟦n⟧').unop ≫ ((F.op.commShiftIso n).hom.app (op (X.unop⟦n⟧))).unop :=
by
apply Quiver.Hom.op_inj
dsimp [opShiftFunctorEquivalence]
rw [assoc, F.op_commShiftIso_hom_app_assoc _ _ _ (add_neg_cancel n), map_comp,
map_shiftFunctorCompIsoId_inv_app_assoc, op_comp, op_comp_assoc, op_comp_assoc, NatTrans.naturality_assoc, op_map,
Iso.inv_hom_id_app_assoc, Quiver.Hom.unop_op]
