quasiIsoAt_of_comp_right — Mathlib

English

If φ′ is a quasi-isomorphism and φ ≫ φ′ is a quasi-isomorphism, then φ is a quasi-isomorphism.

Русский

Если φ′ — квазиизоморфизм, и φ ≫ φ′ — квазиизоморфизм, то φ — квазиизоморфизм.

LaTeX

$$$\text{If } QI(\varphi') \text{ and } QI(\varphi \circ \varphi') \text{ then } QI(\varphi).$$$

Lean4

theorem quasiIsoAt_of_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i]
    [hφ' : QuasiIsoAt φ' i] [hφφ' : QuasiIsoAt (φ ≫ φ') i] : QuasiIsoAt φ i :=
  by
  rw [quasiIsoAt_iff_isIso_homologyMap] at hφ' hφφ' ⊢
  rw [homologyMap_comp] at hφφ'
  exact IsIso.of_isIso_comp_right (homologyMap φ i) (homologyMap φ' i)

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