instAbelianModules

Mathlib.AlgebraicGeometry.Modules.Sheaf

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.instAbelianModules

English

For any scheme X, the category X.Modules of modules over X is an Abelian category.

Русский

Для любой схемы X категория модулей над X является абелевой категорией.

LaTeX

$$$\mathrm{Abelian} (X\!:\!Modules).$$$

Lean4

noncomputable instance : Abelian X.Modules :=
  inferInstance

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

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

Разделы

Аффилиация

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