English
A comprehensive associativity identity for three and more composed shift-related morphisms in the SmallShiftedHom setting.
Русский
Полная ассоциативность для трёх и более композиций сдвиг-производных морфизмов в контексте SmallShiftedHom.
LaTeX
$$$\text{comp}_\text{assoc} \;\; (\alpha,\beta,\gamma) \;\; \Rightarrow \; (\alpha.\beta) .\gamma = \alpha.(\beta.\gamma)$$$
Lean4
theorem comp_assoc {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w} W M X Z] [HasSmallLocalizedShiftedHom.{w} W M X T]
[HasSmallLocalizedShiftedHom.{w} W M Y Z] [HasSmallLocalizedShiftedHom.{w} W M Y T]
[HasSmallLocalizedShiftedHom.{w} W M Z T] [HasSmallLocalizedShiftedHom.{w} W M Z Z]
[HasSmallLocalizedShiftedHom.{w} W M T T] (α : SmallShiftedHom.{w} W X Y a₁) (β : SmallShiftedHom.{w} W Y Z a₂)
(γ : SmallShiftedHom.{w} W 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
apply (equiv W W.Q).injective
simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]
