functorHasLeftDual

Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monoidal.functorHasLeftDual

Lean4

instance functorHasLeftDual [LeftRigidCategory D] (F : C ⥤ D) : HasLeftDual F
    where
  leftDual :=
    { obj := fun X => ᘁ(F.obj X)
      map := fun f => ᘁ(F.map (inv f))
      map_comp := fun f g => by simp [comp_leftAdjointMate] }
  exact :=
    { evaluation' :=
        { app := fun _ => ε_ _ _
          naturality := fun X Y f => by simp [tensorHom_def, leftAdjointMate_comp_evaluation] }
      coevaluation' :=
        { app := fun _ => η_ _ _
          naturality := fun X Y f => by simp [tensorHom_def, coevaluation_comp_leftAdjointMate_assoc] } }

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

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

Разделы

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

Аффилиация

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