quasiIso_iff_isIso_homologyMap' — Mathlib

English

For φ: S1 → S2 with homology data h1, h2, there is an equivalence: φ is a quasi-isomorphism iff the homologyMap' φ h1 h2 is an isomorphism.

Русский

Для φ: S1 → S2 с данными гомологии h1, h2 справедливо: φ является квазиизоморфизмом тогда и только тогда, когда homologyMap' φ h1 h2 является изоморфизмом.

LaTeX

$$$\operatorname{QuasiIso}(φ) \iff \operatorname{IsIso}(\text{homologyMap}'(φ,h_1,h_2))$$$

Lean4

theorem quasiIso_iff_isIso_homologyMap' (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
    QuasiIso φ ↔ IsIso (homologyMap' φ h₁ h₂) :=
  quasiIso_iff_isIso_leftHomologyMap' _ _ _

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