instHasHomologyObjOppositeSymmUnopFunctorOp

English

If φ: K → L is a morphism of complexes, then φ is a quasi-iso at degree i in the original category iff φ^{op} is a quasi-iso at i after applying the opposite functor, provided HasHomology i holds for both sides.

Русский

Если φ: K → L — морфизм между комплексами, то φ является квазиизоморфизмом в степени i в исходной категории тогда и только тогда, когда φ^{op} является квазиизоморфизмом в той же степени после применения противоположного функторa, при условии существования гомологии в i-ой степени для обеих сторон.

LaTeX

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

Lean4

instance (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : ((unopFunctor _ _).obj (op K)).HasHomology i :=
  by
  dsimp
  infer_instance

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