quasiIso_unopMap — Mathlib

English

If φ: S1 → S2 is a morphism in the opposite category and φ is a quasi-isomorphism, then unopMap φ is also a quasi-isomorphism.

Русский

Если φ: S1 → S2 является морфизмом в противоположной категории и φ — квазиизоморфизм, то unopMap φ тоже квазиизоморфизм.

LaTeX

$$$\operatorname{QuasiIso}(φ) \Rightarrow \operatorname{QuasiIso}(\operatorname{unopMap}(φ))$$$

Lean4

theorem quasiIso_unopMap {S₁ S₂ : ShortComplex Cᵒᵖ} [S₁.HasHomology] [S₂.HasHomology] [S₁.unop.HasHomology]
    [S₂.unop.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] : QuasiIso (unopMap φ) :=
  by
  rw [← quasiIso_opMap_iff]
  change QuasiIso φ
  infer_instance

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