English
Let f be a morphism X → Y in a category with A-shifts. Then the shifted morphisms f⟦i⟧'⟦j⟧' satisfy a coherence relation expressing that shifting by i and then j is naturally compatible with first shifting by j and then i, up to the shift-commutation isomorphisms.
Русский
Пусть f: X → Y — морфизм в категории, где имеются сдвиги по A. Тогда отображение f после сдвигов i и j удовлетворяет соотношению, показывающему совместимость сдвигов в порядке i, затем j и сначала j, затем i, с учётом изоморфизмов, описывающих коммутативность сдвигов.
LaTeX
$$$ f⟦i⟧'⟦j⟧' = (shiftComm X i j).hom ≫ f⟦j⟧'⟦i⟧' ≫ (shiftComm Y i j).hom $$$
Lean4
/-- When shifts are indexed by an additive commutative monoid, then shifts commute. -/
theorem shiftComm' (i j : A) : f⟦i⟧'⟦j⟧' = (shiftComm _ _ _).hom ≫ f⟦j⟧'⟦i⟧' ≫ (shiftComm _ _ _).hom :=
by
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]
dsimp
simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]
