English
Let F: C → D be a functor carrying a commutative shift structure by an additive monoid A, and X an object of C with a, b ∈ A satisfying a + b = 0. Then the inverse shift-composition isomorphism is preserved by F, i.e. F maps the inverse of the shift functor identity iso at X to the corresponding inverse iso in D, multiplied on the right by the inverses coming from the commutation isomorphisms for a and b.
Русский
Пусть F: C → D — функтор, который совместим с действиями сдвига по аддитивному моноиду A, и пусть X — объект C, а a, b ∈ A удовлетворяют a + b = 0. Тогда обратная изоморфия композиции сдвигов сохраняется под F: отображение F отображает инверсию изоморфии identity-shift на X на соответствующую инверсию в D, умноженную справа на инверсии, полученные из коммShift-изоморфий для a и b.
LaTeX
$$$F.map ((shiftFunctorCompIsoId C a b h).inv.app X) = (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) \u2261 ((F.commShiftIso a).inv.app X)\\,⟪b⟧' \u2261 (F.commShiftIso b).inv.app (X⟦a⟧)$$$
Lean4
@[simp, reassoc]
theorem map_shiftFunctorCompIsoId_inv_app [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) :
F.map ((shiftFunctorCompIsoId C a b h).inv.app X) =
(shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
((F.commShiftIso a).inv.app X)⟦b⟧' ≫ (F.commShiftIso b).inv.app (X⟦a⟧) :=
by
rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp, Iso.hom_inv_id_app, F.map_id,
map_shiftFunctorCompIsoId_hom_app]
simp only [comp_obj, id_obj, Category.assoc, Iso.hom_inv_id_app_assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
Functor.map_id, Category.id_comp]
