English
If a short complex S has a homology, there is a canonical isomorphism between the homology of the opposite complex S.op and the opposite of the homology of S. This is a natural isomorphism of the homology functor with respect to taking opposites
Русский
У короткого комплекса S есть каноническое изоморфное отображение между гомологией противоположного комплекса S.op и противоположностью гомологии самого S. Это естественное изоморование для гомологии при взятии противоположного.
LaTeX
$$S.op.homology ≅ Opposite.op(S.homology)$$
Lean4
/-- The canonical isomorphism `S.op.homology ≅ Opposite.op S.homology` when a short
complex `S` has homology. -/
noncomputable def homologyOpIso [S.HasHomology] : S.op.homology ≅ Opposite.op S.homology :=
S.op.leftHomologyIso.symm ≪≫ S.leftHomologyOpIso ≪≫ S.rightHomologyIso.symm.op
