English
Let φ: K → L and φ′: L → M be morphisms of homogeneous complexes. If the i-th homology maps H_i(φ) and H_i(φ′) are isomorphisms, then the i-th homology map of their composition H_i(φ′ ∘ φ) is also an isomorphism.
Русский
Пусть φ: K → L и φ′: L → M — морфизмы однородных комплексов. Если соответствующие i‑я гомологические отображения H_i(φ) и H_i(φ′) являются изоморфизмами, то и отображение H_i(φ′ ∘ φ) является изоморфизмом.
LaTeX
$$$\text{For each } i,\quad H_i(K) \xrightarrow{H_i(\varphi)} H_i(L) \xrightarrow{H_i(\varphi')} H_i(M),\quad \text{if } H_i(\varphi)\ \text{and}\ H_i(\varphi')\ \text{are isomorphisms, then } H_i(\varphi'\circ \varphi) \,\text{is an isomorphism.}$$$
Lean4
instance quasiIsoAt_comp (φ : 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] at hφ hφ' ⊢
rw [Functor.map_comp]
exact ShortComplex.quasiIso_comp _ _
