moduleCatCyclesIso — Mathlib

English

There is an isomorphism between abstract cycles and the concrete left-hand homology data described for module categories.

Русский

Существует изоморфизм между абстрактными циклами и конкретным описанием данных левого гомологии для модулярной категории.

LaTeX

$$$\text{moduleCatCyclesIso}: S.cycles \cong S.moduleCatLeftHomologyData.K$$$

Lean4

/-- Given a short complex `S` of modules, this is the isomorphism between
the abstract `S.cycles` of the homology API and the more concrete description as
`LinearMap.ker S.g`. -/
noncomputable def moduleCatCyclesIso : S.cycles ≅ S.moduleCatLeftHomologyData.K :=
  S.moduleCatLeftHomologyData.cyclesIso

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