quasiIso_map_of_preservesRightHomology

English

If F preserves left homology data and respects isomorphisms, then a quasi-isomorphism φ between S1 and S2 is sent to a quasi-isomorphism by F.mapShortComplex.map.

Русский

Если F сохраняет данные левой гомологии и сохраняет/отражает изоморфизмы, то квазиизоморфизм φ между S1 и S2 отображается в квазиизоморфизм через F.mapShortComplex.map.

LaTeX

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

Lean4

instance quasiIso_map_of_preservesRightHomology [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂]
    [QuasiIso φ] : QuasiIso (F.mapShortComplex.map φ) :=
  by
  have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default
  have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
  rw [(γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]
  infer_instance

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