opposite

Mathlib.CategoryTheory.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Category.opposite

Lean4

/-- The opposite category. -/
@[stacks 001M]
instance opposite : Category.{v₁} Cᵒᵖ where
  comp f g := (g.unop ≫ f.unop).op
  id X := (𝟙 (unop X)).op

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru