English
Let F: C → D be shift-commuting. For X ∈ C^op and n ∈ ℤ, F maps the inverse unit at X to the corresponding expression in D, namely ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj X.unop))).unop ≫ (((F.op).commShiftIso n).hom.app X).unop⟦n⟧' ≫ ((F.commShiftIso n).inv.app _).
Русский
Пусть F: C → D коммутирует сдвиги. Для X ∈ C^op и n ∈ ℤ отображение F инверсной единицы в X даёт выражение, соответствующее в D: ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj X.unop))).unop ≫ (((F.op).commShiftIso n).hom.app X).unop⟦n⟧' ≫ ((F.commShiftIso n).inv.app _).
LaTeX
$$$F\left((\operatorname{opShiftFunctorEquivalence} C \; n).unitIso.inv.app X\right).unop = ((\operatorname{opShiftFunctorEquivalence} D \; n).unitIso.inv.app (\operatorname{op}(F.obj X.unop))).unop \;\circ\; ((F.op).commShiftIso n).hom.app X.unop \;\circ\; (F.commShiftIso n)^{-1}$$$
Lean4
@[reassoc]
theorem map_opShiftFunctorEquivalence_unitIso_inv_app_unop (X : Cᵒᵖ) (n : ℤ) :
F.map ((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj X.unop))).unop ≫
(((F.op).commShiftIso n).hom.app X).unop⟦n⟧' ≫ ((F.commShiftIso n).inv.app _) :=
by
rw [← cancel_mono (F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop), ← F.map_comp, ← unop_comp,
Iso.hom_inv_id_app, map_opShiftFunctorEquivalence_unitIso_hom_app_unop, assoc, assoc, Iso.inv_hom_id_app_assoc, ←
Functor.map_comp_assoc, ← unop_comp]
simp
