English
Let F1, F2, F3 be functors with A-shift structure and let τ: F1 ⇒ F2 be a natural transformation with a shift-compatibility. Then the a-shift of τ at X is equal to the conjugation by the commShift iso: (τ.app X)⟦a⟧' = (F1.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F2.commShiftIso a).hom.app X.
Русский
Пусть F1, F2, F3 — функторы с A-сдвигами и τ: F1 ⇒ F2 — натрансформа́ция, совместимая со сдвигами. Тогда a-сдвиг объекта X удовлетворяет: (τ.app X)⟦a⟧' = (F1.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F2.commShiftIso a).hom.app X.
LaTeX
$$$(\\tau.app X)\\,⟦a⟧' = (F_1.commShiftIso a).inv.app X \\\\; \\circ \\\\; \\tau.app (X\\,⟦a⟧) \\\\; \\circ \\\\; (F_2.commShiftIso a).hom.app X$$$
Lean4
@[reassoc]
theorem shift_app_comm (a : A) (X : C) :
(F₁.commShiftIso a).hom.app X ≫ (τ.app X)⟦a⟧' = τ.app (X⟦a⟧) ≫ (F₂.commShiftIso a).hom.app X :=
congr_app (shift_comm τ a) X
