quasiIso_of_comp_left — 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 quasiIso_of_comp_left (φ : 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_left φ φ']
  infer_instance

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