rightHomologyOpIso — Mathlib

English

If φ: S1 ⟶ S2 is an isomorphism and both S1,S2 have right homology, then opcyclesMap φ is an isomorphism.

Русский

Если φ: S1 ⟶ S2 — изоморфизм и S1,S2 имеют правую гомологию, то opcyclesMap φ является изоморфизмом.

LaTeX

$$IsIso\left(\mathrm{opcyclesMap}(\varphi)\right)$$

Lean4

/-- The right homology in the opposite category of the opposite of a short complex identifies
to the left homology of this short complex. -/
noncomputable def rightHomologyOpIso [S.HasLeftHomology] : S.op.rightHomology ≅ Opposite.op S.leftHomology :=
  S.leftHomologyData.op.rightHomologyIso

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