quasiIso_iff — Mathlib

English

Let φ: S1 → S2 with left homology data h1, h2 on S1, S2. Then φ is a quasi-isomorphism if and only if the left 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₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
    (γ : LeftHomologyMapData φ h₁ h₂) : QuasiIso φ ↔ IsIso γ.φH :=
  by
  rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]
  constructor
  · intro h
    haveI : IsIso (γ.φH ≫ (LeftHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (LeftHomologyData.homologyIso h₁).hom _
    exact IsIso.of_isIso_comp_right _ (LeftHomologyData.homologyIso h₂).inv
  · intro h
    infer_instance

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