mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso

English

For a functor F that preserves homology, the quasi-isomorphisms in C become inverted after applying mapHomologicalComplex UpToQuasiIso and then localizing with Q.

Русский

Для функторa F, поддерживающего гомологию, квазиизоморфизмы в C становятся инвертируемыми после применения mapHomologicalComplex UpToQuasiIso и локализации Q.

LaTeX

$$$ \operatorname{IsInvertedBy}\bigl( (F.mapHomologicalComplex\ c)\circ \mathrm{Q} \bigr) = \text{true}.$$$

Lean4

theorem mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso :
    (HomologicalComplex.quasiIso C c).IsInvertedBy (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q) := by
  apply (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).inverts

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