Qh — Mathlib · SciLib

English

The functor Qh localizes the homotopy category to the derived category: Qh: HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C.

Русский

Функтор Qh локализует гомотопическую категорию в производную: Qh: HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C.

LaTeX

$$$Q\\!h:\\; \\mathrm{HomotopyCategory}(C,\\text{ComplexShape.up }\\mathbb{Z}) \\longrightarrow \\mathrm{DerivedCategory}(C).$$$

Lean4

/-- The localization functor `HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C`. -/
def Qh : HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C :=
  HomologicalComplexUpToQuasiIso.Qh

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