quasiIsoAt_opFunctor_map_iff — Mathlib

English

For morphism φ: K → L in the base category with HasHomology in every i, the opFunctor map φ.op retains a quasi-isomorphism status exactly when φ is a quasi-isomorphism.

Русский

Для морфизма φ: K → L во всез степенях гомологии opFunctor сохраняет статус квазиизоморфизма точно тогда, когда φ является квазиизоморфизмом.

LaTeX

$$$\\text{QuasiIso}((\\mathrm{opFunctor} \\; _\\_).map φ.op) \\iff \\text{QuasiIso} φ$$$

Lean4

@[simp]
theorem quasiIsoAt_opFunctor_map_iff {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i]
    [L.HasHomology i] : QuasiIsoAt ((opFunctor _ _).map φ.op) i ↔ QuasiIsoAt φ i :=
  by
  simp only [quasiIsoAt_iff]
  exact ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

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