moduleCatHomologyIso — Mathlib

English

There is a canonical isomorphism between the homology of S and the left-hand homology data.

Русский

Существует каноническое изоморфизм между гомологией S и данными левой гомологии.

LaTeX

$$$ S.homology \cong S.moduleCatLeftHomologyData.H $$$

Lean4

/-- Given a short complex `S` of modules, this is the isomorphism between
the abstract `S.homology` of the homology API and the more explicit
quotient of `LinearMap.ker S.g` by the image of
`S.moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g`. -/
noncomputable def moduleCatHomologyIso : S.homology ≅ S.moduleCatLeftHomologyData.H :=
  S.moduleCatLeftHomologyData.homologyIso

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