English
A repeated formulation of the hom-app for the shift-commutativity under F, expressing the interplay of commShiftIso, shiftFunctor and shiftFunctorAdd.
Русский
Повторная формулировка гом-аппа для коммутативности сдвигов под F, выражающая взаимодействие commShiftIso, shiftFunctor и shiftFunctorAdd.
LaTeX
$$$ (F.map ((shiftFunctorComm C a b).hom.app X)) = (F.commShiftIso b).hom.app (X⟦a⟧) ≫ ((F.commShiftIso a).hom.app X)⟦b⟧' ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫ ((F.commShiftIso b).inv.app X)⟦a⟧' ≫ (F.commShiftIso a).inv.app (X⟦b⟧) $$$
Lean4
theorem map_shiftFunctorComm_hom_app [F.CommShift B] (X : C) (a b : B) :
F.map ((shiftFunctorComm C a b).hom.app X) =
(F.commShiftIso b).hom.app (X⟦a⟧) ≫
((F.commShiftIso a).hom.app X)⟦b⟧' ≫
(shiftFunctorComm D a b).hom.app (F.obj X) ≫
((F.commShiftIso b).inv.app X)⟦a⟧' ≫ (F.commShiftIso a).inv.app (X⟦b⟧) :=
by
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add a b)) X
simp only [comp_obj, CommShift.isoAdd_hom_app, ← cancel_epi (F.map ((shiftFunctorAdd C a b).inv.app X)),
← F.map_comp_assoc, Iso.inv_hom_id_app, F.map_id, Category.id_comp] at eq
simp only [shiftFunctorComm_eq D a b _ rfl]
dsimp
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc, ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]
dsimp
rw [Functor.map_comp]
simp only [NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' (add_comm b a))) X, CommShift.isoAdd'_hom_app,
Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id,
Category.id_comp, comp_obj, Category.comp_id]
