instPreservesZeroMorphismsHomologyFunctor

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor

English

The homology functor preserves zero morphisms: it sends zeros to zeros.

Русский

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

LaTeX

$$$$ \text{HomologyFunctor}(C,c,i) \; \text{ preserves zero morphisms} $$$$

Lean4

instance [CategoryWithHomology C] : (homologyFunctor C c i).PreservesZeroMorphisms where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru