English
In a preadditive category with a shift structure, for any a,b,c ∈ M with b + a = c, and α1, α2: X → Y of degree a, and β: Y → Z of degree b, the composition distributes over addition: (α1 + α2).comp β h = α1.comp β h + α2.comp β h.
Русский
В преддобавительной категории с структурой сдвига, для любых a,b,c ∈ M с b + a = c и α1, α2: X → Y степени a, β: Y → Z степени b, композиция распределяется по сложению: (α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 comp_add [∀ (a : M), (shiftFunctor C a).Additive] {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, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
