instAbelian

Mathlib.CategoryTheory.Action.Limits

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

English

If V is Abelian, then Action V G is Abelian (i.e., an Abelian category).

Русский

Если V абелева, то Action V G является абелевой категорией.

LaTeX

$$$[\text{Abelian}(V)] \Rightarrow [\mathrm{Abelian}(\mathrm{Action}(V,G))]$$$

Lean4

noncomputable instance [Abelian V] : Abelian (Action V G) :=
  abelianOfEquivalence abelianAux.functor

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

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

Разделы

Аффилиация

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