singleObjHomologySelfIso_inv_homologyι

English

The inverse of the cycles self-iso composed with the homologyι map equals the inverse of the corresponding self-homology iso.

Русский

Обратное от cycles self-iso, композиция с homologyι, равно обратному изоморфизму гомологии.

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 singleObjHomologySelfIso_inv_homologyι :
    (singleObjHomologySelfIso _ _ _).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso _ _ _).hom :=
  by
  rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc,
    homology_π_ι, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom]

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