instIsRepresentableCompOppositeOpObjTypeYonedaObjRightAdjointObjIsDefined

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

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

English

For F with partialLeftAdjoint, the object F.op ⋙ yoneda.obj Y.obj is representable; i.e., IsRepresentable holds.

Русский

Для F с частичным левым сопряжением объект F.op ⋙ yoneda.obj Y.obj является представляемым.

LaTeX

$$$\text{IsRepresentable}(F.op \circ \mathrm{yoneda.obj}(Y.obj))$$$

Lean4

instance (Y : F.PartialRightAdjointSource) : IsRepresentable (F.op ⋙ yoneda.obj Y.obj) :=
  Y.property

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

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

Разделы

Аффилиация

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