cyclesOpIso — Mathlib

English

There is a canonical isomorphism between the i-th cycles of the opposite of a homological complex K and the opposite of its opcycles; i.e. for every i, K.op.cycles i is isomorphic to op(K.opcycles i).

Русский

Для любого индекса i существует канонический изоморфизм между i-й циклической частью противоположного гомологического комплекса K и противоположностью (op) его opcycles.

LaTeX

$$$K^{op}.cycles(i) \cong \operatorname{op}(K^{opcycles}(i))$$$

Lean4

/-- The canonical isomorphism `K.op.cycles i ≅ op (K.opcycles i)`. -/
def cyclesOpIso : K.op.cycles i ≅ op (K.opcycles i) :=
  (K.sc i).cyclesOpIso

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