instIsIsoMapCochainComplexIntQ — Mathlib

English

The functor Q is the localization functor from CochainComplex to DerivedCategory.

Русский

Функтор Q является локализационным отображением от CochainComplex к DerivedCategory.

LaTeX

$$$Q:\\; \\text{CochainComplex } C\\; \\mathbb{Z} \\longrightarrow \\text{DerivedCategory } C.$$$

Lean4

instance {K L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f] : IsIso (Q.map f) :=
  Localization.inverts Q (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) _ (inferInstanceAs (QuasiIso f))

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