leftHomologyOpIso — Mathlib

English

There exists a natural isomorphism between the left homology of S in the opposite category and the right homology of S, i.e., leftHomologyOpIso [S.HasRightHomology] : S.op.leftHomology ≅ Opposite.op S.rightHomology.

Русский

Существует естественный изоморфизм между левой гомологией S в противоположной категории и правой гомологией S, то есть leftHomologyOpIso : S.op.leftHomology ≅ Opposite.op S.rightHomology.

LaTeX

$$leftHomologyOpIso\left(S\right) : S.op.leftHomology \cong Opposite.op\; S.rightHomology$$

Lean4

/-- The left homology in the opposite category of the opposite of a short complex identifies
to the right homology of this short complex. -/
noncomputable def leftHomologyOpIso [S.HasRightHomology] : S.op.leftHomology ≅ Opposite.op S.rightHomology :=
  S.rightHomologyData.op.leftHomologyIso

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