instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso

English

For every i, the homology functor sends quasi-isomorphisms to isomorphisms.

Русский

Для каждого i гомологическая функция отображает квазиизоморфизмы в изоморфизмы.

LaTeX

$$$ \forall i,\; \operatorname{IsIso}\bigl(H_i(f)\bigr) \text{ whenever } \operatorname{QuasiIso}(f). $$$

Lean4

instance : (HomotopyCategory.quotient C c ⋙ Qh).IsLocalization (HomologicalComplex.quasiIso C c) :=
  Functor.IsLocalization.of_iso _ (quotientCompQhIso C c).symm

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