homologyOp — Mathlib

English

There is a canonical isomorphism between the homology of K.op at i and the opposite of the homology of K at i: K.op.homology i ≅ op (K.homology i).

Русский

Существует каноническое изоморфизм между гомологией K.op в i-ой степени и противоположной гомологией K в i-ой: K.op.homology i ≅ op (K.homology i).

LaTeX

$$\\n\\def\\{H_i(K^{op})\\} \\cong \\mathrm{op}(H_i(K))$$

Lean4

/-- If `K` is a homological complex, then the homology of `K.op` identifies to
the opposite of the homology of `K`. -/
def homologyOp (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.homology i ≅ op (K.homology i) :=
  (K.sc i).homologyOpIso

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