English
Let W be a category with finite products and zero morphisms, and let c be a complex shape with index set ι. For any j ∈ ι, the construction that assigns to every object X ∈ W the object consisting of a single component at position j (and zero elsewhere) defines an additive functor. In particular, the map on morphisms is additive: map(f+g) = map(f) + map(g).
Русский
Пусть W — категория с нулевыми морфизмами, и пусть c задаёт форму комплекса с индексами ι. Для любого j ∈ ι конструкция, которая сопоставляет каждому объекту X ∈ W единичный компонент на позиции j (и нулевые компоненты в остальных местах), образует аддитивный функтор. В частности, отображение морфизмов сохраняет сложение: map(f+g) = map(f) + map(g).
LaTeX
$$$\bigl(\mathrm{single} \, W \, c \, j\bigr) \text{ is an additive functor.}$$$
Lean4
instance (W : Type*) [Category W] [Preadditive W] [HasZeroObject W] [DecidableEq ι] (j : ι) : (single W c j).Additive
where map_add {_ _ f g} := by ext; simp [single]
