instHasColimitsCommAlgCat — Mathlib

English

For a fixed commutative ring R, the category of commutative R-algebras has all small colimits.

Русский

Для фиксированного коммутативного кольца R категория коммутативных R-алгебр имеет все малые колимиты.

LaTeX

$$$\mathrm{HasColimits}(\mathrm{CommAlgCat}(R))$$$

Lean4

instance : HasColimits (CommAlgCat.{u} R) :=
  Adjunction.has_colimits_of_equivalence (commAlgCatEquivUnder (.of R)).functor

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