homologyπ_singleObjHomologySelfIso_hom

English

For any f: C.X0 ⟶ X and any n, the (n+1)th component of the inverse image under toSingle₀Equiv is zero.

Русский

Для любого f: C.X0 ⟶ X и любого n, (n+1)-ая компонента образа через обратное toSingle₀Equiv равна нулю.

LaTeX

$$$((\\mathrm{toSingle}_0^{\\mathrm{Equiv}} C X)^{-1} f)_{n+1} = 0$$$

Lean4

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

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