functorHom

Mathlib.CategoryTheory.Functor.FunctorHom

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

Lean4

/-- Composition of `homObjFunctor` with the co-Yoneda embedding, i.e. Hom(F ⊗ coyoneda(-), G).
When `F G : C ⥤ Type max v' v u`, this is the internal hom of `F` and `G`: see
`Mathlib/CategoryTheory/Closed/FunctorToTypes.lean`. -/
def functorHom (F G : C ⥤ D) : C ⥤ Type max v' v u :=
  coyoneda.rightOp ⋙ homObjFunctor.{v} F G

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

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

Разделы

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

Аффилиация

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