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.

  • map_smul : ∀ {X Y : C} (f : X Y) (r : R), (r f) = r f

    the functor induces a linear map on morphisms

An additive functor F is R-linear provided is an R-module morphism.