instHasColimitsOfShapePresheaf

Mathlib.Topology.Sheaves.Limits

URI: https://scilib.ai/kg/mathlib#TopCat.instHasColimitsOfShapePresheaf

English

If J is a shape category and C has colimits, then Presheaf C X has colimits of shape J.

Русский

Если J — категория формы и C имеет колимиты, то прешейфы C X имеют колимиты формы J.

LaTeX

$$$[HasColimitsOfShape J C] \\Rightarrow [HasColimitsOfShape J (Presheaf C X)]$$$

Lean4

instance [HasColimitsOfShape J C] (X : TopCat) : HasColimitsOfShape J (Presheaf C X) :=
  functorCategoryHasColimitsOfShape

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

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

Разделы

Аффилиация

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