quasiIso_iff_isIso_rightHomologyMap'

English

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

Русский

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

LaTeX

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

Lean4

theorem quasiIso_iff_isIso_rightHomologyMap' (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂) :=
  by
  have γ : RightHomologyMapData φ h₁ h₂ := default
  rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]

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