instAbelian

Mathlib.Algebra.Category.FGModuleCat.Abelian

URI: https://scilib.ai/kg/mathlib#FGModuleCat.instAbelian

English

The category FGModuleCat(k) of finitely generated modules over a Noetherian ring k is an abelian category.

Русский

Категория FGModuleCat(k) конечноп порожденных модулей над кольцом k абелева при условии, что k — кольцо Нётерова.

LaTeX

$$$\\mathrm{Abelian}(\\mathrm{FGModuleCat}(k))$$$

Lean4

instance : Abelian (FGModuleCat k) :=
  Abelian.ofCoimageImageComparisonIsIso

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

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

Разделы

Аффилиация

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