instAB5ModuleCat — Mathlib

English

The category ModuleCat R is AB5 for any ring R, i.e., it has exact filtered colimits, inherited from its abelian structure.

Русский

Категория ModuleCat R является AB5 для любого кольца R: она имеет точные фильтрованные колимиты благодаря своей абелевой структуре.

LaTeX

$$$\text{AB5}(\text{ModuleCat } R)$$$

Lean4

instance : AB5 (ModuleCat.{u} R) where
  ofShape J _ _ := HasExactColimitsOfShape.domain_of_functor J (forget₂ (ModuleCat R) AddCommGrpCat)

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