homologyFunctor_inverts_quasiIso — Mathlib

English

For every index i, the i-th homology functor sends quasi-isomorphisms to isomorphisms; equivalently, it inverts quasi-isomorphisms with respect to i.

Русский

Для каждого индекса i функция i-й гомологии отправляет квазиизоморфизмы в изоморфизмы; эквивалентно, она обращает квазиизоморфизмы в отношении i.

LaTeX

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

Lean4

theorem homologyFunctor_inverts_quasiIso (i : ι) : (quasiIso C c).IsInvertedBy (homologyFunctor C c i) :=
  fun _ _ _ hf => hf i

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