zero_apply — Mathlib

English

For any x in the underlying object, the composition equals zero: (forget₂.map S.g) ((forget₂.map S.f) x) = 0.

Русский

Для любого элемента x из соответствующего объекта композиция даёт 0: (forget.map S.g)( (forget.map S.f) x ) = 0.

LaTeX

$$$$ ((\\mathrm{forget}_{C} \\ Ab).map S.g) \\Bigl(((\\mathrm{forget}_{C} \\ Ab).map S.f) x\\Bigr) = 0. $$$$

Lean4

@[simp]
theorem zero_apply [Limits.HasZeroMorphisms C] [(forget₂ C Ab).PreservesZeroMorphisms] (S : ShortComplex C)
    (x : (forget₂ C Ab).obj S.X₁) : ((forget₂ C Ab).map S.g) (((forget₂ C Ab).map S.f) x) = 0 :=
  by
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]
  rfl

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