hasLeftHomology_iff_unop

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

English

For S a ShortComplex in Cᵒᵖ, S.HasLeftHomology is equivalent to S.unop.HasRightHomology.

Русский

Для S в категории Cᵒᵖ, левая гомология эквивалентна правой гомологии у S.unop.

LaTeX

$$$ HasLeftHomology(S) \iff HasRightHomology(S^{unop}) $$$

Lean4

theorem hasLeftHomology_iff_unop (S : ShortComplex Cᵒᵖ) : S.HasLeftHomology ↔ S.unop.HasRightHomology :=
  S.unop.hasRightHomology_iff_op.symm

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

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

Разделы

Аффилиация

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