English
Let C be a preadditive category with a shift by a monoid M. For any objects X,Y,Z in C and any a,b,c in M with b + a = c, and any β in ShiftedHom Y Z b, the composition of the zero morphism of degree a with β equals the zero morphism of degree c; that is, (0 : ShiftedHom X Y a).comp β h = 0.
Русский
Пусть C — предадитивная категория с сдвигами по моноида M. Для любых объектов X, Y, Z в C и любых a, b, c в M с условием b + a = c, а также β в ShiftedHom Y Z b существует, тогда композиция нулевого морфизма степени a с β, где h = b + a = c, равна нулю морфизмy степени c: (0 : ShiftedHom X Y a).comp β h = 0.
LaTeX
$$$\\forall a,b,c\\in M\\,,\\forall β\\in \\mathrm{ShiftedHom}\\,YZ\\,b\\,,\\forall h\\; (b+a=c),\\quad (0:\\mathrm{ShiftedHom}\\,XY\\,a).\\mathrm{comp}\\,β\\,h = 0.$$$
Lean4
@[simp]
theorem zero_comp (a : M) {b c : M} (β : ShiftedHom Y Z b) (h : b + a = c) : (0 : ShiftedHom X Y a).comp β h = 0 := by
rw [comp, Limits.zero_comp]
