English
Assume φ: K → L and φ′: L → M with i-th homologies defined. If H_i(φ) is an isomorphism, then H_i(φ ≫ φ′) is an isomorphism if and only if H_i(φ′) is an isomorphism.
Русский
Пусть φ: K → L и φ′: L → M с определенными i-й гомологиями. Тогда H_i(φ ≫ φ′) изоморфизм тогда и только тогда, когда H_i(φ′) изоморфизм (при условии, что H_i(φ) изоморфизм).
LaTeX
$$$\text{If } H_i(\varphi) \text{ is iso, then } H_i(\varphi \circ \varphi') \text{ is iso } \iff H_i(\varphi') \text{ is iso.}$$$
Lean4
theorem quasiIsoAt_iff_comp_left (φ : 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_left φ φ' i
· intro
infer_instance
