quasiIso_iff_isIso_leftHomologyMap'

English

For φ: S1 → S2 with left homology data h1, h2, the quasi-isomorphism status of φ is equivalent to the iso-ness of the leftHomologyMap' φ h1 h2.

Русский

Для φ: S1 → S2 с данными левой гомологии h1, h2 условие квазиизоморфности φ эквивалентно тому, что leftHomologyMap' φ h1 h2 является изоморфизмом.

LaTeX

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

Lean4

theorem quasiIso_iff_isIso_leftHomologyMap' (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂) :=
  by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]

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