instAdditiveHomologicalComplexQuotient

Mathlib.Algebra.Homology.HomotopyCategory

URI: https://scilib.ai/kg/mathlib#HomotopyCategory.instAdditiveHomologicalComplexQuotient

English

The quotient category carries an additive structure, i.e., addition of morphisms is well-defined and compatible with composition.

Русский

Квотированная категория обладает аддитивной структурой: сложение морфизмов определено и совместимо с композицией.

LaTeX

$$$(\text{quotient } V c).\mathrm{Additive}$$$

Lean4

instance : (quotient V c).Additive where

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

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

Разделы

Аффилиация

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