instPreservesZeroMorphismsHomologicalComplexExtendFunctor

Mathlib.Algebra.Homology.Embedding.Extend

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor

English

If the ambient category has a zero morphism, the extension functor along an embedding preserves zero morphisms.

Русский

Если в категории есть нулевой морфизм, катогория-расширение вдоль вложения сохраняет нулевые морфизмы.

LaTeX

$$$(e\\extendFunctor C).PreservesZeroMorphisms$$$

Lean4

instance [HasZeroMorphisms C] : (e.extendFunctor C).PreservesZeroMorphisms where

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

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

Разделы

Аффилиация

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