instHasHomologyUnopOfOpposite

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.instHasHomologyUnopOfOpposite

English

If S has Homology, then its unop S.unop has Homology.

Русский

Если у S есть гомология, то у S.unop есть гомология.

LaTeX

$$$HasHomology(S.unop)$$$

Lean4

instance (S : ShortComplex Cᵒᵖ) [HasHomology S] : HasHomology S.unop :=
  HasHomology.mk' S.homologyData.unop

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

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

Разделы

Аффилиация

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