English
The localization Qh inverts quasi-isomorphisms in the homotopy setting; i.e., quasi-isomorphisms map to isomorphisms under Qh.
Русский
Локализация Qh в гомотопическом контексте обращает квазиизоморфизмы в изоморфизмы; т.е. квазиизоморфизмы отображаются в изоморфизмы при применении Qh.
LaTeX
$$$ (HomotopyCategory.quasiIso(C,c)).IsInvertedBy(Qh). $$$
Lean4
instance :
(HomotopyCategory.quotient C (ComplexShape.up ℤ)).IsLocalization (HomologicalComplex.homotopyEquivalences _ _) :=
(ComplexShape.up ℤ).quotient_isLocalization (fun n => ⟨n - 1, by simp⟩) C
