instQuasiIsoAtOppositeMapSymmOpFunctorOp

English

If φ is a morphism with HasHomology, then there is a canonical equivalence of quasi-isomorphisms between φ and its image under the opposite-map construction, in the At-level sense.

Русский

Для φ с гомологиями существует каноническое соответствие между квазиизоморфизмом φ и его изображением через противоположное отображение.

LaTeX

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

Lean4

instance {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt φ i] :
    QuasiIsoAt ((opFunctor _ _).map φ.op) i :=
  by
  rw [quasiIsoAt_opFunctor_map_iff]
  infer_instance

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