exact_iff_isZero_rightHomology

Mathlib.Algebra.Homology.ShortComplex.Exact

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

English

For a ShortComplex with HasHomology, S is exact iff its right homology is zero.

Русский

Для краткого комплекса S с гомологией S точен тогда и только тогда, когда правая гомология равна нулю.

LaTeX

$$$S.Exact \\iff IsZero S.rightHomology$$$

Lean4

theorem exact_iff_isZero_rightHomology [S.HasHomology] : S.Exact ↔ IsZero S.rightHomology :=
  RightHomologyData.exact_iff _

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

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

Разделы

Аффилиация

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