singleObjCyclesSelfIso_inv_homologyπ

English

The inverse of the cycles self-iso composed with the homology π map equals the inverse of the isomorphism giving the homology at j.

Русский

Обратное от cycles self-iso, композиция с гомологии π, даёт обратный изоморфизм, задающий гомологию на j.

LaTeX

$$$(\\mathrm{singleObjCyclesSelfIso} \\, c \\, j \, A)^{-1} \\circ (((\\mathrm{single} \\, C \\, c \\, j).\\mathrm{obj} A).homologyπ \\, j) = (\\mathrm{singleObjHomologySelfIso} \\, c \\, j \\, A)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem singleObjCyclesSelfIso_inv_homologyπ :
    (singleObjCyclesSelfIso _ _ _).inv ≫ ((single C c j).obj A).homologyπ j = (singleObjHomologySelfIso _ _ _).inv := by
  simp [singleObjCyclesSelfIso, singleObjHomologySelfIso]

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