instAbelian

Mathlib.Algebra.Homology.HomologicalComplexAbelian

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

English

If every degreewise map is short exact, then the overall short complex is short exact.

Русский

Если каждый компонент на каждом уровне образует короткий точный хвост, то весь короткий комплекс точный.

LaTeX

$$$S.ShortExact \\text{ iff } \\forall i, (S.map (eval C c i)).ShortExact$$$

Lean4

noncomputable instance : Abelian (HomologicalComplex C c) where

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

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

Разделы

Аффилиация

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