quasiIso_comp — Mathlib

English

If φ: S1 → S2 and φ': S2 → S3 are quasi-iso, then φ ≫ φ' is quasi-iso.

Русский

Если φ: S1 → S2 и φ': S2 → S3 — квазиизоморфизмы, то φ ≫ φ' — квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(φ) \land \text{QuasiIso}(φ') \Rightarrow \text{QuasiIso}(φ \gg φ')$$$

Lean4

instance quasiIso_comp (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] : QuasiIso (φ ≫ φ') :=
  by
  rw [quasiIso_iff] at hφ hφ' ⊢
  rw [homologyMap_comp]
  infer_instance

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