English
Let J be a category, R : J ⥤ D a diagram in D with a limit cone c, and assume that F : C ⥤ D has right adjoint objects defined at every R.obj j (for all j ∈ J), and that C has limits of shape J. Then the right adjoint object exists at the limit, i.e. F.rightAdjointObjIsDefined (limit R).
Русский
Пусть J — категория, R : J ⥤ D — диаграмма в D с пределом, и предположим, что F : C ⥤ D имеет определённые правая сопряжённая на каждом объекте R.j, для всех j ∈ J, и что C имеет пределы формы J. Тогда правая сопряжённая на предел существует: F.rightAdjointObjIsDefined (limit R).
LaTeX
$$$[HasLimit R] \\; [HasLimitsOfShape J C] \\; (\\forall j : J, \\ F.rightAdjointObjIsDefined (R.obj j)) \\Rightarrow F.rightAdjointObjIsDefined (limit R)$$$
Lean4
theorem rightAdjointObjIsDefined_of_isLimit {J : Type*} [Category J] {R : J ⥤ D} {c : Cone R} (hc : IsLimit c)
[HasLimitsOfShape J C] (h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) : F.rightAdjointObjIsDefined c.pt :=
(representableByCompYonedaObjOfIsLimit (R := ObjectProperty.lift _ R h) hc (limit.isLimit _)).isRepresentable
