hasColimits_commRingCat — Mathlib

English

The category CommRingCat has all small colimits; the construction is carried out by taking the colimit in the ambient ring-like category and transporting to CommRingCat.

Русский

Категория CommRingCat имеет все малые колимиты; конструкция строится через colimit в надкатегории колец и переносится в CommRingCat.

LaTeX

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

Lean4

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

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