quasiIsoAt_of_retract — Mathlib

English

If f is a retract of f' and f' induces a quasi-isomorphism at i, then f does also at i.

Русский

Если f является разложимым на retract из f' и f' индуцирует квазиизоморфизм на i, то и f индуктивирует его на i.

LaTeX

$$QuasiIsoAt f i$$

Lean4

theorem quasiIsoAt_of_retract {f : K ⟶ L} {f' : K' ⟶ L'} (h : RetractArrow f f') (i : ι) [K.HasHomology i]
    [L.HasHomology i] [K'.HasHomology i] [L'.HasHomology i] [hf' : QuasiIsoAt f' i] : QuasiIsoAt f i :=
  by
  rw [quasiIsoAt_iff] at hf' ⊢
  have : RetractArrow ((shortComplexFunctor C c i).map f) ((shortComplexFunctor C c i).map f') :=
    h.map (shortComplexFunctor C c i).mapArrow
  exact ShortComplex.quasiIso_of_retract this

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