quasiIso_map_iff — Mathlib

English

For a functor F, the quasi-isomorphism of the mapped short complexes is equivalent to a quasi-isomorphism of the original map under certain preservation assumptions.

Русский

Для функторa F квазиизоморфизм отображения S1→S2 сохраняется эквивалентно квазиизоморфизму отображения φ в исходной карте при некоторых предположениях сохранения.

LaTeX

$$$\text{QuasiIso}(F.mapShortComplex.map\,\phi) \Longleftrightarrow \text{QuasiIso}(\phi)$$$

Lean4

theorem quasiIso_map_iff [(F.mapShortComplex.obj S₁).HasHomology] [(F.mapShortComplex.obj S₂).HasHomology]
    [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F] : QuasiIso (F.mapShortComplex.map φ) ↔ IsIso (F.map ψr.φH) :=
  (ψr.map F).quasiIso_iff

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