singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv

English

The inverse of the canonical cycles self-iso maps to the standard iCycles map via a simple equality of composites; this equality expresses the compatibility between the self-iso and the iCycles map.

Русский

Обратное канонического цикла-объекта равно iCycles-мару через простое тождество композитов; это выражает совместимость между самогомологическим изоморфизмом и отображением iCycles.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv :
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv = ((single C c j).obj A).homologyπ j := by
  simp only [← cancel_mono (singleObjHomologySelfIso _ _ _).hom, assoc, Iso.inv_hom_id, comp_id,
    homologyπ_singleObjHomologySelfIso_hom]

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