homologyIsoSc'_hom_ι — Mathlib

English

There is an inverse isomorphism on the homology side with respect to the sc' configuration.

Русский

Существует обратное изоморфирование на стороне гомологии в конфигурации sc'.

LaTeX

$$$ (K.sc' i j k).homologyπ \circ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv \circ K.homologyπ j $$$

Lean4

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

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