English
Let φ: K → L and φ′: L → M with i-th homology defined. If φ′ is a quasi-isomorphism at i and φ ≫ φ′ is a quasi-isomorphism at i, then φ is a quasi-isomorphism at i.
Русский
Пусть φ: K → L и φ′: L → M имеет определенную i-ю гомологию. Если φ′ является квазиизоморфизмом в i-й степени и φ ≫ φ′ — квазиизоморфизм в i-й степени, тогда φ — квазиизоморфизм в i-й степени.
LaTeX
$$$\text{If } QI_{i}(\varphi') \text{ and } QI_{i}(\varphi \circ \varphi') \text{ then } QI_{i}(\varphi).$$$
Lean4
theorem quasiIsoAt_iff_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i]
[hφ' : QuasiIsoAt φ' i] : QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i :=
by
constructor
· intro
exact quasiIsoAt_of_comp_right φ φ' i
· intro
infer_instance
