instIsLocalizationHomotopyCategoryQhQuasiIso

English

The functor Qh induces a localization of the homotopy category with respect to quasi-isomorphisms; i.e., Qh localizes along quasi-isomorphisms.

Русский

Функтор Qh индуцирует локализацию гомотопической категории по отношению к квазиизоморфизмам.

LaTeX

$$$\text{IsLocalization}(HomotopyCategory.quasiIso(C,c), Qh).$$$

Lean4

/-- The category `HomologicalComplexUpToQuasiIso C c` which was defined as a localization of
`HomologicalComplex C c` with respect to quasi-isomorphisms also identify to a localization
of the homotopy category with respect to quasi-isomorphisms. -/
instance : HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.quasiIso C c) :=
  Functor.IsLocalization.of_comp (HomotopyCategory.quotient C c) Qh (HomologicalComplex.homotopyEquivalences C c)
    (HomotopyCategory.quasiIso C c) (HomologicalComplex.quasiIso C c) (homotopyEquivalences_le_quasiIso C c)
    (HomotopyCategory.quasiIso_eq_quasiIso_map_quotient C c)

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