instHasHomologyUnopOfOpposite — Mathlib

English

If K is a homological complex, then its unop also carries HasHomology in every degree i, reflecting the preservation of homology under unop.

Русский

Если K — гомологический комплекс, то его unop также имеет гомологию в каждом степени i; сохранение гомологии под операцией unop.

LaTeX

$$$\\forall i,\\; (K^{unop}).HasHomology(i) \\;\\text{whenever}\\; K.HasHomology(i)$$$

Lean4

instance (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : K.unop.HasHomology i :=
  (inferInstance : (K.sc i).unop.HasHomology)

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