map_sub

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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

English

A additive functor preserves subtraction of morphisms.

Русский

Добавитивный функтор сохраняет вычитание морфизмов.

LaTeX

$$$F.map(f - g) = F.map(f) - F.map(g)$$$

Lean4

@[simp]
theorem map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=
  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_sub _ _

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

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

Разделы

Аффилиация

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