rightAdjointObjIsDefined_limit — Mathlib

English

If R : J ⥤ D has a limit and F.rightAdjointObjIsDefined holds for every R.obj j, then F.rightAdjointObjIsDefined (limit R).

Русский

Если у диаграммы R : J ⥤ D существует предел, и для каждого R.obj j правый сопряжённый объекта определён, то он определён и на пределе limit R.

LaTeX

$$$[HasLimit R] \\; [HasLimitsOfShape J C] \\; (\\forall j : J, F.rightAdjointObjIsDefined (R.obj j)) \\Rightarrow F.rightAdjointObjIsDefined (limit R)$$$

Lean4

theorem rightAdjointObjIsDefined_limit {J : Type*} [Category J] (R : J ⥤ D) [HasLimit R] [HasLimitsOfShape J C]
    (h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) : F.rightAdjointObjIsDefined (limit R) :=
  rightAdjointObjIsDefined_of_isLimit (limit.isLimit R) h

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