comp_zero — Mathlib

English

In a shifted setting, composing with the zero morphism on the right yields the zero morphism: β.comp 0 h = 0.

Русский

В условиях сдвига композиция справа с нулевым морфизмом даёт нулевой морфизм: β.comp 0 h = 0.

LaTeX

$$$\\beta.\\mathrm{comp} 0\\ h = 0$$$

Lean4

@[simp]
theorem comp_zero [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms] {a : M} (β : ShiftedHom X Y a) {b c : M}
    (h : b + a = c) : β.comp (0 : ShiftedHom Y Z b) h = 0 := by
  rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]

Похожие утверждения