isIso_Q_map_iff_quasiIso — Mathlib

English

For any cochain map φ, the map Q.map φ is an isomorphism if and only if φ is a quasi-isomorphism.

Русский

Для любой пары комплексов сопоставления φ, отображение Q.map φ является изоморфизмом тогда и только тогда, когда φ является квазиизоморфизмом.

LaTeX

$$$IsIso\ (Q.map\ \varphi) \iff\ QuasiIso\ \varphi$$$

Lean4

theorem isIso_Q_map_iff_quasiIso {K L : CochainComplex C ℤ} (φ : K ⟶ L) : IsIso (Q.map φ) ↔ QuasiIso φ := by
  apply HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso

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