English
Let a1, a2, a3 ∈ A and X ∈ C with given equalities h12, h23, h123 expressing associativity of addition. Then the natural isomorphisms from shifting by a1+a2 then a3 equals shifting by a1 then a2+a3 satisfy the specified associativity condition on their hom components at X.
Русский
Пусть a1, a2, a3 ∈ A и X ∈ C с данными равенствами h12, h23, h123, выражающими associativity сложения. Тогда гомоморфизмы из композиции сдвигов удовлетворяют соответствующему ассоциативному условию на компоненте X.
LaTeX
$$$ (\\mathrm{shiftFunctorAdd'} \\, C \\, a_1 \\_ {2} a_3 \\_ {1} a_{1_2_3} (..)).hom.app X \\, \\gg \\left( (\\mathrm{shiftFunctorAdd'} \\, C \\, a_1 a_2 a_{1_2} h_{12}).hom.app X \\right)^{\\langle a_3 \\rangle} \\\\ = \\\\ (\\mathrm{shiftFunctorAdd'} \\, C \\, a_1 a_2_3 a_{1_2_3} (..)).hom.app X \\\\ gg \\left( (\\mathrm{shiftFunctorAdd'} \\, C a_2 a_3 a_{2_3} h_{23}).hom.app (X\\langle a_1 \\rangle) \\right) $$$
Lean4
@[reassoc]
theorem shiftFunctorAdd'_assoc_hom_app (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
(shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃])).hom.app X ≫
((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)⟦a₃⟧' =
(shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃])).hom.app X ≫
(shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app (X⟦a₁⟧) :=
by simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X
