partialRightAdjointObj

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

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

Lean4

/-- Given `F : C ⥤ D`, this is `F.partialRightAdjoint` on objects: it sends
`X : D` such that `F.rightAdjointObjIsDefined X` holds to an object of `C`
which represents the functor `F ⋙ coyoneda.obj (op X.obj)`. -/
noncomputable def partialRightAdjointObj (Y : F.PartialRightAdjointSource) : C :=
  (F.op ⋙ yoneda.obj Y.obj).reprX

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

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

Разделы

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

Аффилиация

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