respectsIso_quasiIso — Mathlib

English

The class of quasi-isomorphisms is stable under isomorphisms of arrows; in particular, if f is a quasi-isomorphism and f is isomorphic to g, then g is a quasi-isomorphism as well.

Русский

Класс квазиизоморфизмов стабилен относительно изоморфизмов стрел; если f является квазиизоморфизмом и f изоморфен g, то и g является квазиизоморфизмом.

LaTeX

$$$ f \cong g \implies (\operatorname{QuasiIso}(f) \iff \operatorname{QuasiIso}(g)). $$$

Lean4

instance respectsIso_quasiIso : (quasiIso C c).RespectsIso :=
  by
  apply MorphismProperty.RespectsIso.of_respects_arrow_iso
  intro f g e hf i
  exact ((MorphismProperty.isomorphisms C).arrow_mk_iso_iff ((homologyFunctor C c i).mapArrow.mapIso e)).1 (hf i)

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