English
Let F: C → D commute with shifts. For X ∈ C^op and n ∈ ℤ, F.map of the counit inverse app at X equals the specified composite: ((F.op.commShiftIso n).inv.app (op (X.unop⟦n⟧))).unop ≫ (((F.commShiftIso n).hom.app X.unop).unop⟦n⟧').unop ≫ ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj X.unop))).unop.
Русский
Пусть F: C → D коммутирует сдвиги. Для X ∈ C^op и n ∈ ℤ, отображение F.map инверсной аппликации counit в X равняется заданной композиции.
LaTeX
$$$F.map ((\operatorname{opShiftFunctorEquivalence} C n).counitIso.inv.app X).unop = ((\operatorname{F.op}.commShiftIso n).inv.app (op (X.unop\langle n \rangle))).unop \circ (((F.commShiftIso n).hom.app X.unop).unop\langle n \rangle').unop \circ ((\operatorname{opShiftFunctorEquivalence} D n).counitIso.inv.app (op (F.obj X.unop))).unop$$$
Lean4
@[reassoc]
theorem map_opShiftFunctorEquivalence_counitIso_inv_app_unop (X : Cᵒᵖ) (n : ℤ) :
F.map ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
((F.op.commShiftIso n).inv.app (op (X.unop⟦n⟧))).unop ≫
(((F.commShiftIso n).hom.app X.unop).op⟦n⟧').unop ≫
((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj X.unop))).unop :=
by
rw [← cancel_epi (F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop), ← F.map_comp, ← unop_comp,
Iso.inv_hom_id_app, map_opShiftFunctorEquivalence_counitIso_hom_app_unop]
dsimp
simp only [map_id, assoc, ← Functor.map_comp_assoc, ← unop_comp, Iso.inv_hom_id_app_assoc, ← op_comp,
Iso.inv_hom_id_app]
simp
