instAdditiveHomologyFunctor

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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

English

An isomorphism exists between the pOpcycles of K and the corresponding structure in sc'.

Русский

Существует изоморфизм между pOpcycles K и соответствующей структурой в sc'.

LaTeX

$$$ (K.sc' i j k).pOpcycles \cong K.pOpcycles j $$$

Lean4

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

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

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

Разделы

Аффилиация

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