English
Assume all i-th homology groups exist. Then φ ≫ φ′ is a quasi-isomorphism if and only if φ′ is a quasi-isomorphism, provided φ is itself a quasi-isomorphism.
Русский
Пусть существуют все i‑ые гомологии. Тогда φ ≫ φ′ — квазиизоморфизм тогда и только тогда, когда φ′ — квазиизоморфизм, если φ сам является квазиизоморфизмом.
LaTeX
$$$\text{If }\forall i, K.HasHomology i, L.HasHomology i, M.HasHomology i,\ h\varphi: QI(\varphi) \text{ and } h\varphi': QI(\varphi') \text{ then } QI(\varphi \circ \varphi').$$$
Lean4
theorem quasiIso_iff_comp_left (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
[∀ i, M.HasHomology i] [hφ : QuasiIso φ] : QuasiIso (φ ≫ φ') ↔ QuasiIso φ' := by
simp only [quasiIso_iff, quasiIsoAt_iff_comp_left φ φ']
