pOpcycles_singleObjOpcyclesSelfIso_inv

English

The inverse of the cycles self-iso, composed with the homologyπ map, equals the homology π iso in the opposite direction.

Русский

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

LaTeX

$$$(\\mathrm{singleObjCyclesSelfIso} \\; c \\; j \\; A)^{-1} \\circ (\\mathrm{homology\\pi}_j) = (\\mathrm{singleObjHomologySelfIso} \\; c \\; j \\; A)^{-1} $$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_singleObjOpcyclesSelfIso_inv :
    ((single C c j).obj A).pOpcycles j ≫ (singleObjOpcyclesSelfIso _ _ _).inv = (singleObjXSelf c j A).hom :=
  by
  have := ((single C c j).obj A).isIso_iCycles j _ rfl (by simp)
  rw [← cancel_epi (((single C c j).obj A).iCycles j), ← HomologicalComplex.homology_π_ι_assoc,
    homologyι_singleObjOpcyclesSelfIso_inv, homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_hom]

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