opInv

Mathlib.CategoryTheory.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.opInv

Lean4

/-- Take the "unopposite" of a functor is functorial.
-/
@[simps]
def opInv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ where
  obj F := op F.unop
  map
    α :=
    Quiver.Hom.op
      { app := fun X => (α.app (op X)).unop
        naturality := fun _ _ f => Quiver.Hom.op_inj <| (α.naturality f.op).symm }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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