English
Let F1, F2, F3: C ⥤ D with A-shifts and τ: F1 ⟶ F2, τ′: F2 ⟶ F3 with a natural isomorphism e: F1 ≅ F2. Then the app-shift relation holds after shifting via shift functors: (τ.app X)⟦a⟧' = (F1.commShiftIso a).inv.app X ≫ τ.app (X⟦a⟧) ≫ (F2.commShiftIso a).hom.app X.
Русский
Пусть F1, F2, F3: C ⥤ D с A-сдвигами и τ: F1 ⟶ F2, τ′: F2 ⟶ F3 с изоморфизмом e: F1 ≅ F2. Тогда равенство на приложении к сдвигу сохраняется: (τ.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 app_shift (a : A) (X : C) :
τ.app (X⟦a⟧) = (F₁.commShiftIso a).hom.app X ≫ (τ.app X)⟦a⟧' ≫ (F₂.commShiftIso a).inv.app X := by
simp [shift_app_comm_assoc τ a X]
