English
Quasi-isomorphisms agree with their images under the quotient map; i.e., the quasi-iso relation is transported along the quotient functor.
Русский
Квазиизоморфизм согласуется со своим изображением через тождественно применяемую квотированную карту; т. е. отношение квазиизоморфизм переносится вдоль квази-облика.
LaTeX
$$$ \operatorname{QuasiIso}_{Homotopy}(C,c)\,\bigl( f \bigr) = \operatorname{QuasiIso}(C,c,f) \text{ is equivalent to } \operatorname{QuasiIso}(C,c,((quotient\ C\ c).map\ f)). $$$
Lean4
theorem quasiIso_eq_quasiIso_map_quotient : quasiIso C c = (HomologicalComplex.quasiIso C c).map (quotient C c) :=
by
ext ⟨K⟩ ⟨L⟩ f
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective f
constructor
· intro hf
rw [quotient_map_mem_quasiIso_iff] at hf
exact MorphismProperty.map_mem_map _ _ _ hf
· rintro ⟨K', L', g, h, ⟨e⟩⟩
rw [← quotient_map_mem_quasiIso_iff] at h
exact ((quasiIso C c).arrow_mk_iso_iff e).1 h
