English
Let F: C → D be a functor that commutes with shifts by integers. For every X in the opposite of C and every integer n, F maps the unit of the shift equivalence at X to the composite of the corresponding shift-isomorphisms and the unit at the image, i.e. F maps ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop to the composition (F.commShiftIso n).hom.app _ ≫ (((F.op).commShiftIso n).inv.app X).unop⟦n⟧' ≫ ((opShiftFunctorEquivalence D n).unitIso.hom.app (op _)).unop.
Русский
Пусть F: C → D — функтор, совместимый по сдвигам на целые числа. Для каждого Y ∈ C^op и целого n верно, что F отображает единицу эквивалентности сдвига на Y в композицию, состоящую из соответствующих изоморфизмов сдвига и единицы на образе, то есть F отображает unitIso.hom.app X через unop в указанный тройной композит.
LaTeX
$$$\text{Let } F: \mathcal{C} \to \mathcal{D} \text{ satisfy } F \text{ commShift }\mathbb{Z} \text{. For all } X \in \mathcal{C}^{\mathrm{op}}, \ n \in \mathbb{Z}, \\ F\left((\operatorname{opShiftFunctorEquivalence} \mathcal{C} \; n).\mathrm{unitIso}.\mathrm{hom.app}\; X\right).\mathrm{unop} = (F.\mathrm{commShiftIso} n).\mathrm{hom.app}\; _ \\ \quad \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \; \circ \big(((F.op).\mathrm{commShiftIso} n).\mathrm{inv.app} \; X\big).\mathrm{unop} \langle n \rangle' \circ ((\operatorname{opShiftFunctorEquivalence} \mathcal{D} \; n).\mathrm{unitIso}.\mathrm{hom.app} (\operatorname{op} _)).\mathrm{unop}$$$
Lean4
@[reassoc]
theorem map_opShiftFunctorEquivalence_unitIso_hom_app_unop (X : Cᵒᵖ) (n : ℤ) :
F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop =
(F.commShiftIso n).hom.app _ ≫
(((F.op).commShiftIso n).inv.app X).unop⟦n⟧' ≫ ((opShiftFunctorEquivalence D n).unitIso.hom.app (op _)).unop :=
by
dsimp [opShiftFunctorEquivalence]
simp only [map_comp, unop_comp, Quiver.Hom.unop_op, assoc, map_shiftFunctorCompIsoId_hom_app,
commShiftIso_hom_naturality_assoc, op_commShiftIso_inv_app _ _ _ _ (add_neg_cancel n)]
congr 3
rw [← Functor.map_comp_assoc, ← unop_comp, Iso.inv_hom_id_app]
dsimp
rw [map_id, id_comp]
