isIso_Qh_map_iff — Mathlib

English

For X, Y in the homotopy category, f is an isomorphism after applying Qh iff f is a quasi-isomorphism.

Русский

Для X, Y в гомотопийной категории: изоморфизм после применения Qh эквивалентен квазиизоморфизму.

LaTeX

$$IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C _ f$$

Lean4

theorem isIso_Qh_map_iff {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) :
    IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C _ f :=
  by
  constructor
  · intro hf
    rw [HomotopyCategory.mem_quasiIso_iff]
    intro n
    rw [← NatIso.isIso_map_iff (homologyFunctorFactorsh C n) f]
    dsimp
    infer_instance
  · exact Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _

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