instAdditiveComp

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instAdditiveComp

English

If F: C ⥤ D and G: D ⥤ E are additive functors, then their composite F ⋙ G is additive.

Русский

Если F: C ⥤ D и G: D ⥤ E — добавитивные функторы, то их композиция F ⋙ G является добавитивной.

LaTeX

$$$ (F ⋙ G).Additive$$$

Lean4

instance {E : Type*} [Category E] [Preadditive E] (G : D ⥤ E) [Functor.Additive G] : Additive (F ⋙ G) where

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

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

Разделы

Аффилиация

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