instHasTwoOutOfThreePropertyQuasiIso

English

The collection of quasi-isomorphisms is closed under composition and contains identities; this yields a multiplicative structure on quasi-isomorphisms.

Русский

Система квазиизоморфизм замкнута относительно композиции и содержит тождественные отображения; получается многоквадратическая структура квазиизоморфизмов.

LaTeX

$$$\text{QI} \text{ is closed under composition and contains identities.}$$$

Lean4

instance : (quasiIso C c).HasTwoOutOfThreeProperty
    where
  of_postcomp f g hg
    hfg := by
    rw [mem_quasiIso_iff] at hg hfg ⊢
    rwa [← quasiIso_iff_comp_right f g]
  of_precomp f g hf
    hfg := by
    rw [mem_quasiIso_iff] at hf hfg ⊢
    rwa [← quasiIso_iff_comp_left f g]

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