English
Associativity of composition for ShiftedHom morphisms: composing α with β and then with γ is the same as composing α with (β composed with γ) under the appropriate shift indices, up to the shift-add associativity.
Русский
Ассоциативность композиции morphisms в ShiftedHom: последовательности (α ∘ β) ∘ γ и α ∘ (β ∘ γ) согласованы по индексам сдвига.
LaTeX
$$theorem comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : M} (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) : (α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) = α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h])$$
Lean4
theorem comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : M} (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃)
(h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
(α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) =
α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h]) :=
by
simp only [comp, assoc, Functor.map_comp, shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
← NatTrans.naturality_assoc, Functor.comp_map]
