quasiIso_opMap_iff — Mathlib

English

If φ is a quasi-isomorphism, then its opposite opMap(φ) is also a quasi-isomorphism.

Русский

Если φ является квазиизоморфизмом, то противоположная стрелка opMap(φ) тоже является квазиизоморфизмом.

LaTeX

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

Lean4

theorem quasiIso_opMap_iff (φ : S₁ ⟶ S₂) : QuasiIso (opMap φ) ↔ QuasiIso φ :=
  by
  have γ : HomologyMapData φ S₁.homologyData S₂.homologyData := default
  rw [γ.left.quasiIso_iff, γ.op.right.quasiIso_iff]
  dsimp
  constructor
  · intro h
    apply isIso_of_op
  · intro h
    infer_instance

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