English
Let F be a functor with a shift structure on a monoid M and with a ShiftSequence. For elements m, n, mn ∈ M with mn = m + n and compatible indices a, a′, a″ ∈ M such that a′ = n + a and a″ = m + a′, the shift isomorphism for mn from a to a″ equals the composite of the natural isomorphisms coming from the addition of shifts and the associator, whiskered on the right by F and whiskered on the left by F as appropriate.
Русский
Пусть F — функтор с структурой сдвига над моноидом M и последовательность сдвигов. Пусть элементы m, n, mn ∈ M удовлетворяют mn = m + n и существуют индексы a, a′, a″ ∈ M такие, что a′ = n + a и a″ = m + a′. Тогда изоморфизм сдвига для mn, переходящий из a в a″, равен композиции естественных изоморождений, получаемых из сложения сдвигов, сопряжённой ассоциатором, и подкатегорируемой к F.
LaTeX
$$$F.shiftIso\; mn\; a\; a''\ (by\ rw [\lt- hnm, \lt- ha'', \lt- ha', add_assoc]) = \\ isoWhiskerRight (shiftFunctorAdd' C m n mn hnm) _ \\ \\ll\comp Functor.associator _ _ _ \\ \\ll\ isoWhiskerLeft _ (F.shiftIso n a a' ha') \\ \\ll\ F.shiftIso m a' a'' ha''$$
Lean4
theorem shiftIso_add' (n m mn : M) (hnm : m + n = mn) (a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') :
F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc]) =
isoWhiskerRight (shiftFunctorAdd' C m n _ hnm) _ ≪≫
Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' :=
by
subst hnm
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]
