hasColimits

Mathlib.CategoryTheory.Limits.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.hasColimits

English

If T has colimits, then the arrow category Arrow T has all colimits.

Русский

Если в T существуют колимиты, то Arrow T имеет все колимиты.

LaTeX

$$$\\operatorname{HasColimits}(T) \\Rightarrow \\operatorname{HasColimits}(\\mathrm{Arrow}(T))$$$

Lean4

instance hasColimits [HasColimits T] : HasColimits (Arrow T) :=
  ⟨fun _ _ => inferInstance⟩

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

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

Разделы

Аффилиация

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