inducedFunctor_additive

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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

English

For any C → D, the induced functor (inducedFunctor F) is additive when D is preadditive.

Русский

Для любого отображения F: C → D индуцированный функтор (inducedFunctor F) является аддитивным, если D предаддитивна.

LaTeX

$$$\mathrm{Additive}(\mathrm{inducedFunctor}(F))$$$

Lean4

instance inducedFunctor_additive : Functor.Additive (inducedFunctor F) where

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

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

Разделы

Аффилиация

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