quasiIsoAt_map_of_preservesHomology

English

Let F be a functor preserving homology. If φ is a quasi-isomorphism at i, then the image map (F.map φ) is also a quasi-isomorphism at i.

Русский

Пусть F — отображение сохраняющее гомологию. Тогда если φ — квазиизоморфизм в i-м, то его образ под F.map тоже квазиизоморфизм в i-м.

LaTeX

$$$\text{If } QI_i(\varphi) \text{ and } F \text{ preserves homology, then } QI_i((F.map \varphi)).$$$

Lean4

instance quasiIsoAt_map_of_preservesHomology [hφ : QuasiIsoAt φ i] : QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i :=
  by
  rw [quasiIsoAt_iff] at hφ ⊢
  exact ShortComplex.quasiIso_map_of_preservesLeftHomology F ((shortComplexFunctor C₁ c i).map φ)

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