moduleCatHomology — Mathlib

English

The homology of a short complex in ModuleCat is realized as a concrete quotient built from the left homology data.

Русский

Гомология короткого комплекса в ModuleCat представлена как конкретный фактор-модуль, полученный из левых данных гомологии.

LaTeX

$$moduleCatHomology = moduleCatLeftHomologyData.H$$

Lean4

/-- The homology of a short complex of modules as a concrete quotient. -/
@[deprecated "This abbreviation is now inlined" (since := "2025-05-14")]
abbrev moduleCatHomology :=
  S.moduleCatLeftHomologyData.H

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