English
In a preadditive category with a shift structure, for all a,b,c ∈ M, α1, α2: X → Y a, β: Y → Z b with h: b + a = c, the equality (α1 + α2).comp β h = α1.comp β h + α2.comp β h holds, expressing additivity of composition in shifted contexts.
Русский
В преддобавительной категории с сдвигами для всех a,b,c ∈ M, α1, α2: X→Y степени a, β: Y→Z степени b при h: b+a=c выполняется равенство (α1+α2).comp β h = α1.comp β h + α2.comp β h, выражающее аддитивность композиции в контексте сдвигов.
LaTeX
$$$\\forall a,b,c\\in M\\; (α_1+α_2).\\mathrm{comp}\\ β\\ h = α_1.\\mathrm{comp}\\ β\\ h + α_2.\\mathrm{comp}\\ β\\ h \\quad\\text{for } h:\\; b+a=c$$$
Lean4
@[simp]
theorem add_comp {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
(α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h := by rw [comp, comp, comp, Preadditive.add_comp]
