mapAction_preadditive

Mathlib.CategoryTheory.Action.Limits

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

English

As in 62706, the sum of morphisms behaves additively on hom components.

Русский

Как в 62706, сумма морфизмов ведет себя аддитивно на компонентах hom.

LaTeX

$$$(s.\mathrm{sum} f).\mathrm{hom} = \sum_i (f_i).\mathrm{hom}$$$

Lean4

instance mapAction_preadditive [F.Additive] : (F.mapAction G).Additive where

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

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

Разделы

Аффилиация

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