comp_neg — Mathlib

English

In a shifted setting, the composition with a negated morphism equals the negation of the composition: α.comp(-β) h = - (α.comp β h).

Русский

В условии со сдвигами композиция с отрицательным морфизмом равна отрицанию композиции: α.comp(-β) h = - (α.comp β h).

LaTeX

$$$\\alpha.\\mathrm{comp}(-\\beta)\\ h = -\\alpha.\\mathrm{comp}\\beta\\ h$$$

Lean4

@[simp]
theorem comp_neg [∀ (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 := by
  rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]

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