CategoryTheory.Functor.Linear.map_smul

theorem CategoryTheory.Functor.Linear.map_smul : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{u_4, u_2} C] [inst_2 : CategoryTheory.Category.{u_5, u_3} D] [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D] {F : CategoryTheory.Functor C D} [inst_7 : F.Additive] [self : CategoryTheory.Functor.Linear R F] {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f

This theorem states that the functor induces a linear map on morphisms. In the context of a category theory, given a semiring `R`, categories `C` and `D` where `C` and `D` are preadditive and linear over `R`, and an additive functor `F` from `C` to `D` that is linear over `R`, for any two objects `X` and `Y` in `C` and a morphism `f` from `X` to `Y` and a scalar `r` in `R`, the map of the scaled morphism `r • f` under the functor `F` is equal to the scaling of the map of the morphism `f` under the functor `F` by `r`. In mathematical notation, it states that for all `f` and `r`, `F.map (r • f) = r • F.map f`.

More concisely: Given an additive, linear functor `F` over a semiring `R` between preadditive and linear categories `C` and `D`, for any object `X`, `Y` in `C`, morphism `f : X → Y` in `C`, and scalar `r` in `R`, the diagram `F.map (r • f) ┼ F.map f ⃗ r` commutes. (Here, `┼` denotes the commutativity of diagrams, and `⃗` denotes the scaling of a map by a scalar.)