quasiIso_map_of_preservesLeftHomology

English

If F preserves left homology of S1 and S2 and φ is a quasi-isomorphism, then F.mapShortComplex.map φ is a quasi-isomorphism; conversely, if F preserves and reflects isomorphisms, the reverse implication holds.

Русский

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

LaTeX

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

Lean4

instance quasiIso_map_of_preservesLeftHomology [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂]
    [QuasiIso φ] : QuasiIso (F.mapShortComplex.map φ) :=
  by
  have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default
  have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
  rw [(γ.map F).quasiIso_iff, LeftHomologyMapData.map_φH]
  infer_instance

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