rightAdjointObjIsDefined

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

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

Lean4

/-- Given a functor `F : C ⥤ D`, this is a predicate on objects `X : D` corresponding
to the domain of definition of the (partial) right adjoint of `F`. -/
def rightAdjointObjIsDefined : ObjectProperty D := fun Y ↦ IsRepresentable (F.op ⋙ yoneda.obj Y)

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

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

Разделы

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

Аффилиация

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