quasiIso_map_iff_of_preservesHomology

English

If φ is a quasi-isomorphism, then its image under a functor that preserves homology is a quasi-isomorphism.

Русский

Если φ — квазиизоморфизм, то его образ под функтором, сохраняющим гомологию, также квазиизоморфизм.

LaTeX

$$$QI(\varphi) \Rightarrow QI((F.mapHomologicalComplex c).map \varphi).$$$

Lean4

theorem quasiIso_map_iff_of_preservesHomology [F.ReflectsIsomorphisms] :
    QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ := by
  simp only [quasiIso_iff, quasiIsoAt_map_iff_of_preservesHomology φ F]

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