mathlib documentation


Linear Functors #

An additive functor between two R-linear categories is called linear if the induced map on hom types is a morphism of R-modules.

Implementation details #

functor.linear is a Prop-valued class, defined by saying that for every two objects X and Y, the map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y) is a morphism of R-modules.

theorem category_theory.functor.map_smul {R : Type u_1} [semiring R] {C : Type u_2} {D : Type u_3} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.linear R C] [category_theory.linear R D] (F : C D) [F.additive] [category_theory.functor.linear R F] {X Y : C} (r : R) (f : X Y) : (r f) = r f

F.map_linear_map is an R-linear map whose underlying function is