categoryWithHomology_of_abelian

Mathlib.Algebra.Homology.ShortComplex.Abelian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.categoryWithHomology_of_abelian

← MathLib Explorer

English

The category with homology exists for an abelian category C.

Русский

Для абелиевой категории C существует категория с гомологией.

LaTeX

$$$$ \\text{CategoryWithHomology}(C). $$$$

Lean4

instance _root_.CategoryTheory.categoryWithHomology_of_abelian : CategoryWithHomology C where
  hasHomology S := HasHomology.mk' (HomologyData.ofAbelian S)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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