homologyFunctorFactorsh — Mathlib

English

The derived category homology functor factors via a homotopy-based path; there is a natural isomorphism with a homology functor on the homotopy category.

Русский

Гомологическая функция выводимой категории факторизуется через путь на основе гомотопии; существует естественный изоморфизм с гомологической функцией над гомотопийной категорией.

LaTeX

$$$Q_h \\cdot \\text{homologyFunctor } C \\;n \\cong \\text{HomotopyCategory.homologyFunctor} \\_\\; (\\text{up}) n$$$

Lean4

/-- The homology functor on the derived category is induced by the homology
functor on the homotopy category of cochain complexes. -/
noncomputable def homologyFunctorFactorsh (n : ℤ) : Qh ⋙ homologyFunctor C n ≅ HomotopyCategory.homologyFunctor _ _ n :=
  HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C (ComplexShape.up ℤ) n

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