opcyclesOpIso_hom_naturality — Mathlib

English

The morphism component of the opcycles isomorphism composes naturally with cycles maps under the opposite functor.

Русский

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

LaTeX

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

Lean4

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

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