singleObjHomologySelfIso — Mathlib

English

The 0th component of the inverse image under fromSingle₀Equiv is exactly f, under hf = 0.

Русский

0-я компонента образа через fromSingle₀Equiv равна f при hf = 0.

LaTeX

$$$((\\mathrm{fromSingle}_0^{\\mathrm{Equiv}} C X)^{-1} \\langle f, hf \\rangle)_0 = f$$$

Lean4

/-- The canonical isomorphism `((single C c j).obj A).homology j ≅ A` -/
noncomputable def singleObjHomologySelfIso : ((single C c j).obj A).homology j ≅ A :=
  (((single C c j).obj A).isoHomologyπ _ j rfl rfl).symm ≪≫ singleObjCyclesSelfIso c j A

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