map_nsmul — Mathlib

English

A additive functor preserves natural-number scalar multiplication of morphisms.

Русский

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

LaTeX

$$$F.map(n\\, f) = n\\,F.map(f)$ for $n\\in\\mathbb{N}$$$

Lean4

theorem map_nsmul {X Y : C} {f : X ⟶ Y} {n : ℕ} : F.map (n • f) = n • F.map f :=
  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_nsmul _
    _
      -- You can alternatively just use `Functor.map_smul` here, with an explicit `(r : ℤ)` argument.

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