hasColimit_const_of_isConnected

Mathlib.CategoryTheory.Limits.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasColimit_const_of_isConnected

English

If J is connected, the constant functor (J ⥤ C) with value X has a colimit.

Русский

Если J связано, константный функтор с значением X имеет ко-лимит.

LaTeX

$$$\mathrm{HasColimit}((\mathrm{Functor.const}\ J).\mathrm{obj}\ X)$$$

Lean4

instance hasColimit_const_of_isConnected : HasColimit ((Functor.const J).obj X) :=
  ⟨_, isColimitConstCocone J X⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru