quasiIso_opFunctor_map_iff — Mathlib

English

For morphisms φ between complexes K and L, the opFunctor map φ.op is a quasi-iso iff φ is a quasi-iso (assuming HasHomology everywhere).

Русский

Для морфизмов φ между комплексами K и L отображение через opFunctor, φ.op, является квазиизоморфизмом тогда и только тогда, когда сам φ — квазиизоморфизм (при условии гомологий во всех степенях).

LaTeX

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

Lean4

@[simp]
theorem quasiIso_opFunctor_map_iff {K L : HomologicalComplex V c} (φ : K ⟶ L) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] : QuasiIso ((opFunctor _ _).map φ.op) ↔ QuasiIso φ := by
  simp only [quasiIso_iff, quasiIsoAt_opFunctor_map_iff]

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