π_homologyIsoSc'_inv — Mathlib

English

Naturality of the map on homology with respect to the isomorphism between π and cycles.

Русский

Естественность отображения на гомологии по отношению к изоморфизму между π и циклами.

LaTeX

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

Lean4

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

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