Theorems · Theorem · category theory

CategoryTheory.Functor.Linear.map_smul

∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {D : Type u_3} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Category.{v_2, 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} [self : CategoryTheory.Functor.Linear R F] {X Y : C} (f : X ⟶ Y) (r : R),
  F.map (r • f) = r • F.map f

the functor induces a linear map on morphisms

Defined in

Mathlib.CategoryTheory.Linear.LinearFunctor

Cited by

2 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CategoryTheory.Functor.Linear