opcyclesOpIso_inv_naturality — Mathlib

English

The inverses of the opcycles isomorphisms satisfy a dual naturality relation with op-functor maps.

Русский

Обратные стороны изоморфизмов opcycles удовлетворяют симметричному натуралитному свойству относительно отображений противоположного функторa.

LaTeX

$$(opcyclesMap φ i).op ≫ (K.opcyclesOpIso i).inv = (L.opcyclesOpIso i).inv ≫ opcyclesMap ((opFunctor _ _).map φ.op) _$$

Lean4

@[reassoc]
theorem opcyclesOpIso_inv_naturality :
    (cyclesMap φ i).op ≫ (K.opcyclesOpIso i).inv = (L.opcyclesOpIso i).inv ≫ opcyclesMap ((opFunctor _ _).map φ.op) _ :=
  ShortComplex.opcyclesOpIso_inv_naturality ((shortComplexFunctor V c i).map φ)

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