hasColimits_ringCat — Mathlib

English

The category RingCat has all small colimits; in particular, for every small diagram F: J ⥤ RingCat there exists a colimit object together with a cocone that is universal.

Русский

Категория RingCat имеет все малые колимиты; существует объект-колимит и универсальное коконное отображение.

LaTeX

$$$\text{HasColimits}(\text{RingCat})$$$

Lean4

instance hasColimits_ringCat : HasColimits RingCat where
  has_colimits_of_shape _
    _ :=
    {
      has_colimit := fun F =>
        HasColimit.mk
          { cocone := colimitCocone F
            isColimit := colimitIsColimit F } }

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