English
A general associativity/coherence identity expresses how a triple shift interacts with a triple composition of shifted morphisms, ensuring associativity of shift operations across multiple indices.
Русский
Обобщённое тождество ассоциативности/согласованности показывает, как тройной сдвиг взаимодействует с тройной композицией сдвинутых морфизмов, обеспечивая ассоциативность операций сдвига по нескольким индексам.
LaTeX
$$$ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ ((shiftFunctorAdd C m₂ m₃).hom.app X)⟦m₁⟧' = (shiftFunctorAdd C m₂ m₃).hom.app (X⟦m₁⟧) ≫ ((shiftFunctorComm C m₁ m₂).hom.app X)⟦m₃⟧' ≫ (shiftFunctorComm C m₁ m₃).hom.app (X⟦m₂⟧) $$$
Lean4
@[reassoc]
theorem shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app (m₁ m₂ m₃ : A) (X : C) :
(shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ ((shiftFunctorAdd C m₂ m₃).hom.app X)⟦m₁⟧' =
(shiftFunctorAdd C m₂ m₃).hom.app (X⟦m₁⟧) ≫
((shiftFunctorComm C m₁ m₂).hom.app X)⟦m₃⟧' ≫ (shiftFunctorComm C m₁ m₃).hom.app (X⟦m₂⟧) :=
by
rw [← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)), ←
cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')]
simp only [Category.assoc, Iso.hom_inv_id_app]
dsimp
simp only [Category.id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]
dsimp
simp only [Functor.map_id, Category.comp_id, shiftFunctorComm_eq C _ _ _ rfl, ← shiftFunctorAdd'_eq_shiftFunctorAdd]
dsimp
simp only [Category.assoc, Iso.hom_inv_id_app_assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₃ m₁ (m₂ + m₃) (m₁ + m₃) (m₁ + (m₂ + m₃)) rfl (add_comm m₃ m₁)
(add_comm _ m₁) X,
←
shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₁ m₃ (m₁ + m₂) (m₁ + m₃) (m₁ + (m₂ + m₃)) (add_comm _ _) rfl
(by rw [add_comm m₂ m₁, add_assoc]) X,
shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ (m₁ + m₂) (m₂ + m₃) (m₁ + (m₂ + m₃)) rfl rfl (add_assoc _ _ _) X]
