instAdditiveSheafAddCommGrpCatToSheaf

Mathlib.Algebra.Category.ModuleCat.Sheaf

URI: https://scilib.ai/kg/mathlib#SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf

English

The category of sheaves of modules on a Grothendieck topology is an additive category.

Русский

Категория пучков модулей над Гротендек топологией является аддитивной.

LaTeX

$$$\mathrm{AddCat}(\mathrm{Sh}_{J}(\mathrm{Mod}_R))$$$

Lean4

instance : (toSheaf R).Additive where

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

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

Разделы

Аффилиация

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