instHasHomologyOppositeOp — Mathlib

English

If K is a homological complex, then K^{op} inherits HasHomology in each degree i from K: for every i, K^{op} has homology at i whenever K has homology at i.

Русский

Если K — гомологический комплекс, то у K^{op} имеется гомология в каждом граде i, если она имеется у K в этом граде.

LaTeX

$$$\\forall i,\\; (K^{op}).HasHomology(i) \\iff K.HasHomology(i)$$$

Lean4

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

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