quasiIso_iff_comp_right — Mathlib

English

If φ′ is a quasi-isomorphism, then φ ≫ φ′ is a quasi-isomorphism if and only if φ is a quasi-isomorphism.

Русский

Если φ′ — квазиизоморфизм, то φ ≫ φ′ — квазиизоморфизм тогда и только тогда, когда φ — квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(\varphi \circ \varphi') \iff \text{QuasiIso}(\varphi)$, если $\text{QuasiIso}(\varphi').$$$

Lean4

theorem quasiIso_iff_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
    [∀ i, M.HasHomology i] [hφ' : QuasiIso φ'] : QuasiIso (φ ≫ φ') ↔ QuasiIso φ := by
  simp only [quasiIso_iff, quasiIsoAt_iff_comp_right φ φ']

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