instQuasiIsoOppositeMapSymmOpFunctorOp

English

If K,L are complexes and φ: K → L is a quasi-isomorphism, then the opposite-map is quasi-iso as well, i.e., (opFunctor V c).map φ.op is quasi-iso.

Русский

Если K,L — комплексы и φ: K → L — квазиизоморфизм, то и отображение через противоположный функтор является квазиизоморфизмом: (opFunctor V c).map φ.op.

LaTeX

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

Lean4

instance {K L : HomologicalComplex V c} (φ : K ⟶ L) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i] [QuasiIso φ] :
    QuasiIso ((opFunctor _ _).map φ.op) := by
  rw [quasiIso_opFunctor_map_iff]
  infer_instance

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