rightAdjointObjIsDefined_of_adjunction

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

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

← MathLib Explorer

English

If adj is an adjunction with F ⊣ G, then F.rightAdjointObjIsDefined Y holds for every Y.

Русский

Если дано сопряжение с F ⊣ G, тогда F.rightAdjointObjIsDefined Y определён для каждого Y.

LaTeX

$$$\text{RightAdjointObjIsDefined}(Y)$$$

Lean4

theorem rightAdjointObjIsDefined_of_adjunction {G : D ⥤ C} (adj : F ⊣ G) (Y : D) : F.rightAdjointObjIsDefined Y :=
  (adj.representableBy Y).isRepresentable

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

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

Разделы

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

Аффилиация

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