instHasHomologyOppositeObjSymmOpFunctorOp

English

For morphism φ: K → L of complexes, φ and its op-map have equivalent quasi-isomorphism status componentwise: φ is a quasi-isomorphism in the original category iff φ^{op} is a quasi-isomorphism after applying opFunctor.

Русский

Для морфизма φ: K → L между комплексами эквивалентны квазиизоморфизмы: φ является квазиизоморфизмом в исходной категории тогда и только тогда, когда φ^{op} становится квазиизоморфизмом после применения opFunctor.

LaTeX

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

Lean4

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

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