hasColimit

Mathlib.Algebra.Category.Grp.Colimits

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.hasColimit

English

The category AddCommGrpCat has colimits of shape J for any small J.

Русский

Категория AddCommGrpCat имеет колимиты формы J для любой малой J.

LaTeX

$$$ \mathrm{HasColimitsOfShape } J \; \mathrm{AddCommGrpCat} $$$

Lean4

instance hasColimit [Small.{w} J] (F : J ⥤ AddCommGrpCat.{w}) : HasColimit F := by
  classical exact hasColimit_of_small_quot F inferInstance

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

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

Разделы

Аффилиация

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