instIsLocalizationCochainComplexIntQQuasiIsoUp

English

If f is a quasi-isomorphism, then the induced map Q.map f is an isomorphism in the derived localization.

Русский

Если f — квазиизоморфизм, индуцированное отображение Q.map f является изоморфизмом в локализации производной категории.

LaTeX

$$$\\forall {K,L},\\ [\\text{QuasiIso } f]\\; \\text{IsIso}(\\mathrm{DerivedCategory}.Q.map f).$$$

Lean4

instance : (Q (C := C)).IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) :=
  by
  dsimp only [Q, DerivedCategory]
  infer_instance

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