quasiIso_iff_of_arrow_mk_iso — Mathlib

English

If φ: S1 → S2, φ′: S3 → S4 and Arrow.mk φ is isomorphic to Arrow.mk φ′, then φ is a quasi-isomorphism if and only if φ′ is a quasi-isomorphism.

Русский

Пусть стрелы φ: S1 → S2, φ′: S3 → S4 и Arrow.mk φ изоморфна Arrow.mk φ′; тогда φ является квазиизоморфизм тогда и только тогда, когда φ′ является квазиизоморфизм.

LaTeX

$$$\operatorname{QuasiIso}(φ) \iff \operatorname{QuasiIso}(φ')$$$

Lean4

theorem quasiIso_iff_of_arrow_mk_iso (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄) (e : Arrow.mk φ ≅ Arrow.mk φ') :
    QuasiIso φ ↔ QuasiIso φ' :=
  ⟨fun _ => quasiIso_of_arrow_mk_iso φ φ' e, fun _ => quasiIso_of_arrow_mk_iso φ' φ e.symm⟩

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