Qh_inverts_quasiIso — Mathlib

English

The functor Qh from the homotopy quotient inverts quasi-isomorphisms; i.e., it sends quasi-iso arrows to isomorphisms.

Русский

Функтор Qh из гомотопной факторизации переводит квазиизоморфизмы в изоморфизмы; т. е. он отправляет стрелы квазиизоморфизмов в изоморфизмы.

LaTeX

$$$ (\mathrm{HomotopyCategory.quasiIso}(C,c)).IsInvertedBy(Qh). $$$

Lean4

theorem Qh_inverts_quasiIso : (HomotopyCategory.quasiIso C c).IsInvertedBy Qh :=
  by
  rintro ⟨K⟩ ⟨L⟩ φ
  obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ
  rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ, ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]
  exact (NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2

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