quasiIso_of_comp_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem quasiIso_of_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
    [∀ i, M.HasHomology i] [hφ : QuasiIso φ'] [hφφ' : QuasiIso (φ ≫ φ')] : QuasiIso φ :=
  by
  rw [← quasiIso_iff_comp_right φ φ']
  infer_instance

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