cyclesOpIso_inv_naturality — Mathlib

English

The inverse opcycles map interacts with the inverse of the cycles iso in a natural way.

Русский

Обратный отображатель opcycles естественным образом взаимодействует с обратным изоморфизмом cycles.

LaTeX

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

Lean4

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

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