instQuasiIsoMapOppositeSymmUnopFunctorOp

English

Mirror of the previous result in the unop/op symmetry: the quasi-iso property transfers through unop and op functors in both directions.

Русский

Зеркальное по отношению к предыдущему результату в симметрии unop/op: свойство квазиизоморфизма переносится сквозь функторы unop и op в обе стороны.

LaTeX

$$$\\text{QuasiIso} ((\\mathrm{unopFunctor} V c).map φ.op) \\iff \\text{QuasiIso} φ$$$

Lean4

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

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