π_homologyIsoSc'_hom — Mathlib

English

Inverse homology iso commutes with the ι-parameterized map on homology.

Русский

Обратное гомологии изоморфизма коммутирует с отображением на гомологию, зависящим от ι.

LaTeX

$$$ (K.homologyIsoSc' i j k hi hk).inv \circ K.homologyι = K.homologyι j \circ (K.opcyclesIsoSc' i j k hi hk).inv $$$

Lean4

@[reassoc (attr := simp)]
theorem π_homologyIsoSc'_hom :
    K.homologyπ j ≫ (K.homologyIsoSc' i j k hi hk).hom = (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyπ :=
  by apply ShortComplex.homologyπ_naturality

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