leftAdjointObjIsDefined_colimit — Mathlib

English

If every R.obj(j) has a defined left adjoint object, then the colimit of R also has a defined left adjoint object.

Русский

Если на каждом элементе диаграммы R имеется определённый левый сопряжённый объект, то и колимит R имеет определённый левый сопряжённый объект.

LaTeX

$$$\forall j, F.leftAdjointObjIsDefined(R.obj j) \Rightarrow F.leftAdjointObjIsDefined(\mathrm{colimit}\;R)$$$

Lean4

theorem leftAdjointObjIsDefined_colimit {J : Type*} [Category J] (R : J ⥤ C) [HasColimit R] [HasColimitsOfShape J D]
    (h : ∀ (j : J), F.leftAdjointObjIsDefined (R.obj j)) : F.leftAdjointObjIsDefined (colimit R) :=
  leftAdjointObjIsDefined_of_isColimit (colimit.isColimit R) h

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