instCategoryWithHomologyOpposite — Mathlib

English

If a category C carries a zero-morphism structure and is equipped with a homology structure, then the opposite category C^{op} inherits a homology structure as well.

Русский

Если категория C имеет нулевые морфизмы и структуру гомологии, то противоположная категория C^{op} также обладает структурой гомологии.

LaTeX

$$$\mathrm{HasHomology}(C) \Rightarrow \mathrm{HasHomology}(C^{op})$$$

Lean4

instance [CategoryWithHomology C] : CategoryWithHomology Cᵒᵖ :=
  ⟨fun S => HasHomology.mk' S.unop.homologyData.op⟩

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