homologyUnop

Mathlib.Algebra.Homology.Opposite

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

Lean4

/-- If `K` is a homological complex in the opposite category,
then the homology of `K.unop` identifies to the opposite of the homology of `K`. -/
def homologyUnop (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : K.unop.homology i ≅ unop (K.homology i) :=
  (K.unop.homologyOp i).unop

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

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

Разделы

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

Аффилиация

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