map_zsmul

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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

English

A additive functor preserves integer scalar multiplication of morphisms.

Русский

Добавитивный функтор сохраняет умножение морфизмов на целые числа (Z-скаляры).

LaTeX

$$$F.map(z f) = z (F.map f)$ for $z\\in\\mathbb{Z}$$$

Lean4

theorem map_zsmul {X Y : C} {f : X ⟶ Y} {r : ℤ} : F.map (r • f) = r • F.map f :=
  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_zsmul _ _

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

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

Разделы

Аффилиация

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