instIsGrothendieckAbelianLightCondMod

Mathlib.Condensed.Light.AB

URI: https://scilib.ai/kg/mathlib#LightCondensed.instIsGrothendieckAbelianLightCondMod

English

The category LightCondMod(R) is Grothendieck abelian.

Русский

Категория LightCondMod(R) является абелевой Гротендиккой.

LaTeX

$$$$\text{IsGrothendieckAbelian}(\mathrm{LightCondMod}(R)).$$$$

Lean4

instance : IsGrothendieckAbelian.{u} (LightCondMod.{u} R) :=
  inferInstanceAs (IsGrothendieckAbelian.{u} (Sheaf _ _))

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

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

Разделы

Аффилиация

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