English
Let K and L be objects in the homological complex category with shape c, and let f: K → L. Then the localized image Q.map f is an isomorphism if and only if f is a quasi-isomorphism.
Русский
Пусть K и L — объекты в категории гомологическх комплексoв с формой c, и f: K → L. Тогда образ локализации Q.map f является изоморфизмом тогда и только тогда, когда f является квазиизоморфизмом.
LaTeX
$$$ \operatorname{IsIso}\bigl(Q(map\ f)\bigr) \iff \operatorname{QuasiIso}(C,c,f). $$$
Lean4
theorem isIso_Q_map_iff_mem_quasiIso {K L : HomologicalComplex C c} (f : K ⟶ L) :
IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f :=
by
constructor
· intro h
rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]
intro i
rw [quasiIsoAt_iff_isIso_homologyMap]
refine (NatIso.isIso_map_iff (homologyFunctorFactors C c i) f).1 ?_
dsimp
infer_instance
· intro h
exact Localization.inverts Q (HomologicalComplex.quasiIso C c) _ h
