instQuasiIsoHom — Mathlib

English

The same quasi-isomorphism structure is preserved for homotopy-induced maps under standard categorical constructions.

Русский

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

LaTeX

$$$\text{QuasiIso preserves under standard constructions.}$$$

Lean4

instance : QuasiIso e.hom where
  quasiIsoAt
    n := by
    classical
    rw [quasiIsoAt_iff_isIso_homologyMap]
    exact (e.toHomologyIso n).isIso_hom

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