instQuasiIsoAtMapOppositeSymmUnopFunctorOp

English

If φ is a morphism of homological complexes, then the opposite-map Φ.op preserves the quasi-isomorphism status, i.e., Φ.op is quasi-iso whenever Φ is.

Русский

Если φ — морфизм гомологического комплекса, то отображение через противоположную структуру сохраняет статус квазиизоморфизма: φ^{op} является квазиизоморфизмом тогда и только тогда, когда φ является таковым.

LaTeX

$$$\\text{QuasiIsoAt}(φ, i) \\Rightarrow \\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 ((unopFunctor _ _).map φ.op) i :=
  by
  rw [quasiIsoAt_unopFunctor_map_iff]
  infer_instance

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