English
Let φ: K → L and φ′: L → M be morphisms with i-th homology defined for K, L, M. If H_i(φ) is an isomorphism and H_i(φ ≫ φ′) is an isomorphism, then H_i(φ′) is an isomorphism.
Русский
Пусть φ: K → L и φ′: L → M — морфизмы; если i-я гомологическая карта φ является изоморфизмом, а i-я карта композиции φ ≫ φ′ — тоже изоморфизм, тогда H_i(φ′) является изоморфизмом.
LaTeX
$$$\text{If } H_i(\varphi) \text{ is an isomorphism and } H_i(\varphi \circ \varphi') \text{ is an isomorphism, then } H_i(\varphi') \text{ is an isomorphism.}$$$
Lean4
theorem quasiIsoAt_of_comp_left (φ : 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_left (homologyMap φ i) (homologyMap φ' i)
