quasiIso_map_iff_of_preservesRightHomology

English

If F preserves right homology of S1 and S2 and φ is a quasi-isomorphism, then F.mapShortComplex.map φ is a quasi-isomorphism.

Русский

Если F сохраняет правую гомологию S1 и S2 и φ — квазиизоморфизм, то F.mapShortComplex.map φ — квазиизоморфизм.

LaTeX

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

Lean4

theorem quasiIso_map_iff_of_preservesRightHomology [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂]
    [F.ReflectsIsomorphisms] : QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ :=
  by
  have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default
  rw [γ.quasiIso_iff, (γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]
  constructor
  · intro
    exact isIso_of_reflects_iso _ F
  · intro
    infer_instance

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