English
Given φ: K → L and φ′: K′ → L′ with an isomorphism of arrows e: Arrow.mk φ ≅ Arrow.mk φ′, and assuming all i-th homologies exist for K, L, K′, L′, we have QuasiIso φ ↔ QuasiIso φ′.
Русский
Пусть есть стрелки φ: K → L и φ′: K′ → L′ и изоморфизм стрел e: Arrow.mk φ ≅ Arrow.mk φ′; если для K, L, K′, L′ существуют i‑йи гомологии, то φ квазиизоморфизм тогда и только тогда, когда φ′ квазиизоморфизм.
LaTeX
$$$\text{QuasiIso}(\varphi) \iff \text{QuasiIso}(\varphi')$ при наличии изomорфизма стрел $\text{Arrow.mk }\varphi \cong \text{Arrow.mk }\varphi'.$$$
Lean4
theorem quasiIso_iff_of_arrow_mk_iso (φ : K ⟶ L) (φ' : K' ⟶ L') (e : Arrow.mk φ ≅ Arrow.mk φ') [∀ i, K.HasHomology i]
[∀ i, L.HasHomology i] [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i] : QuasiIso φ ↔ QuasiIso φ' := by
simp [← quasiIso_iff_comp_left (show K' ⟶ K from e.inv.left) φ,
← quasiIso_iff_comp_right φ' (show L' ⟶ L from e.inv.right)]
