English
Let F1, F2 be functors with a fixed A-shift structure, and let τ: F1 ⇒ F2 be a natural transformation compatible with shifts. Then the following equality of natural transformations holds: (F1.commShiftIso a).homo ≫ whiskerRight τ ∘ = whiskerLeft τ ∘ ≫ (F2.commShiftIso a).hom, expressing that shifting commutes with τ up to the commShift isomorphisms.
Русский
Пусть F1, F2 — функторы с заданной структурой сдвига по A, и τ: F1 ⇒ F2 — натуральное преобразование, совместимое с сдвигами. Тогда выполняется равенство натрасформ: (F1.commShiftIso a).hom ≫ whiskerRight τ = whiskerLeft τ ≫ (F2.commShiftIso a).hom, что выражает совместимость сдвига с τ через commShift-изоморфизмы.
LaTeX
$$$(F_1.commShiftIso\ a).hom \\;\\circ\\; \\mathrm{whiskerRight}\tau = \\mathrm{whiskerLeft}\\tau \\;\\circ\\; (F_2.commShiftIso\ a).hom$$$
Lean4
@[reassoc]
theorem shift_comm (a : A) :
(F₁.commShiftIso a).hom ≫ Functor.whiskerRight τ _ = Functor.whiskerLeft _ τ ≫ (F₂.commShiftIso a).hom := by
apply CommShift.shift_comm
