instIsRightAdjointFunctorLim — Mathlib

English

If J is a shape and C has limits of shape J, then the limit functor lim: [J → C] → C has a right adjoint given by the constant diagram functor Δ: C → [J → C].

Русский

Если C имеет пределы формы J, то правая adjoint к пределу существует: лимитный функтор lim: [J → C] → C имеет правого адъюнкта Δ: C → [J → C], соответствующего константной диаграмме.

LaTeX

$$$\operatorname{HasLimitsOfShape}(J, C) \Rightarrow \operatorname{lim} \dashv \Delta$, где \Delta X является константной диаграммой со значением X.$$

Lean4

instance : IsRightAdjoint (lim : (J ⥤ C) ⥤ C) :=
  ⟨_, ⟨constLimAdj⟩⟩

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