English
Let X, Y be objects of C and m, n, p, m', n', p' be in A with hm, hn, hp as zero-sum conditions and h as the relation m+n = p. Then a long equality of composed homs holds, expressing the associativity of multi-shift operations.
Русский
Пусть X, Y — объекты C, а m, n, p, m', n', p' ∈ A удовлетворяют условиям hm, hn, hp и h: m+n = p. Тогда выполняется длинное равенство композиционных гомоморфизмов, выражающее ассоциативность многоразовых сдвигов.
LaTeX
$$$ (\\mathrm{shiftFunctorCompIsoId} \\, C \\, p' p hp).inv.app X = (\\mathrm{shiftFunctorCompIsoId} \\, C n' n hn).inv.app X \\\\gg (\\mathrm{shiftFunctorCompIsoId} \\, C m' m hm).inv.app (X⟦n'⟧)⟦n⟧' \\\\gg (\\mathrm{shiftFunctorAdd'} \\, C m n p h).inv.app (X⟦n'⟧⟦m'⟧) \\\\gg ((\\mathrm{shiftFunctorAdd'} \\, C n' m' p' (by ...)).inv.app X)⟦p⟧' $$$
Lean4
theorem shift_shift' (i j : A) : f⟦i⟧'⟦j⟧' = (shiftAdd X i j).inv ≫ f⟦i + j⟧' ≫ (shiftAdd Y i j).hom := by simp
