quasiIso_iff — Mathlib

English

Let φ: S1 → S2 with right homology data h1, h2 on S1, S2. Then φ is a quasi-isomorphism if and only if the right homology map γ.φH is an isomorphism.

Русский

Пусть φ: S1 → S2 и соответствующие данные правой гомологий h1, h2. Тогда φ — квазиизоморфизм ⇔ соответствующая правая гомологическая карта γ.φH является изоморфизмом.

LaTeX

$$$\operatorname{QuasiIso}(φ) \iff \operatorname{IsIso}(γ.φH)$$$

Lean4

theorem quasiIso_iff {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
    (γ : RightHomologyMapData φ h₁ h₂) : QuasiIso φ ↔ IsIso γ.φH :=
  by
  rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]
  constructor
  · intro h
    haveI : IsIso (γ.φH ≫ (RightHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (RightHomologyData.homologyIso h₁).hom _
    exact IsIso.of_isIso_comp_right _ (RightHomologyData.homologyIso h₂).inv
  · intro h
    infer_instance

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