instIsGrothendieckAbelianModuleCat

Mathlib.Algebra.Category.ModuleCat.AB

URI: https://scilib.ai/kg/mathlib#instIsGrothendieckAbelianModuleCat

English

For any ring R, the category ModuleCat(R) is a Grothendieck abelian category.

Русский

Для любого кольца R категория ModuleCat(R) является абелевой категорией Гротендика.

LaTeX

$$$\mathrm{IsGrothendieckAbelian}(\mathrm{ModuleCat}(R))$$$

Lean4

instance : IsGrothendieckAbelian.{u} (ModuleCat.{u} R) where

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

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

Разделы

Аффилиация

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