quasiIso_of_arrow_mk_iso — Mathlib

English

If Arrow.mk φ ≅ Arrow.mk φ′ and φ is quasi-isomorphic, then φ′ is quasi-isomorphic.

Русский

Если Arrow.mk φ ≅ Arrow.mk φ′ и φ квазиизоморфизм, то φ′ квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(\varphi) \iff \text{QuasiIso}(\varphi')$ under arrow-mk isomorphism.$$

Lean4

theorem quasiIso_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] [hφ : QuasiIso φ] : QuasiIso φ' := by
  simpa only [← quasiIso_iff_of_arrow_mk_iso φ φ' e]

Похожие утверждения