leftHomologyFunctor_additive — Mathlib

English

The left-hand homology functor is additive, i.e., it preserves sums of morphisms across the relevant categories with kernels and cokernels.

Русский

Функтор левой гомологии аддитивен: он сохраняет сумму морфизмов в соответствующих категориях с ядрами и образами.

LaTeX

$$$ (leftHomologyFunctor C).Additive $$$

Lean4

instance leftHomologyFunctor_additive [HasKernels C] [HasCokernels C] : (leftHomologyFunctor C).Additive where

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