opUnopEquiv

Mathlib.CategoryTheory.Opposites

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

Lean4

/-- The equivalence of functor categories induced by `op` and `unop`.
-/
@[simps]
def opUnopEquiv : (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ where
  functor := opHom _ _
  inverse := opInv _ _
  unitIso :=
    NatIso.ofComponents (fun F => F.unop.opUnopIso.op)
      (by
        intro F G f
        dsimp [opUnopIso]
        rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
        congr 1
        cat_disch)
  counitIso := NatIso.ofComponents fun F => F.unopOpIso

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

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

Разделы

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

Аффилиация

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