quasiIso_of_comp_right — Mathlib

English

Let φ: S1 → S2 and φ′: S2 → S3 be morphisms of ShortComplexes. If φ′ is a quasi-isomorphism and the composite φ ∘ φ′ is a quasi-isomorphism, then φ is a quasi-isomorphism.

Русский

Пусть φ: S1 → S2 и φ′: S2 → S3 — морфизмы в ShortComplex. Если φ′ — квазиизоморфизм, а произведение φ ∘ φ′ — квазиизоморфизм, то φ — квазиизоморфизм.

LaTeX

$$$\operatorname{QuasiIso}(\varphi)$, при условии $\operatorname{QuasiIso}(\varphi')$ и $\operatorname{QuasiIso}(\varphi \circ \varphi')$$$

Lean4

theorem quasiIso_of_comp_right (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : QuasiIso φ'] [hφφ' : QuasiIso (φ ≫ φ')] :
    QuasiIso φ := by
  rw [quasiIso_iff] at hφ' hφφ' ⊢
  rw [homologyMap_comp] at hφφ'
  exact IsIso.of_isIso_comp_right (homologyMap φ) (homologyMap φ')

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