instIsLeftAdjointFunctorColim — Mathlib

English

The colimit functor is left adjoint to the constant diagram functor; i.e., colim ⊣ const.

Русский

Функтор колимита является левым сопряжением к константному функтору диаграммы; то есть colim ⊣ const.

LaTeX

$$$ \\text{colim} \\;:\\; (J \\to C) \\to C \\quad \\text{is left adjoint to} \\quad \\text{const} : C \\to (J \\to C)$$$

Lean4

instance : IsLeftAdjoint (colim : (J ⥤ C) ⥤ C) :=
  ⟨_, ⟨colimConstAdj⟩⟩

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