# 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 F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y) is a morphism of R-modules.

class CategoryTheory.Functor.Linear (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] :

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

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

the functor induces a linear map on morphisms

Instances
theorem CategoryTheory.Functor.Linear.map_smul {R : Type u_1} [] {C : Type u_2} {D : Type u_3} [] [] [] [] {F : } [F.Additive] [self : ] {X : C} {Y : C} (f : X Y) (r : R) :
F.map (r f) = r F.map f

the functor induces a linear map on morphisms

@[simp]
theorem CategoryTheory.Functor.map_smul {R : Type u_1} [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {X : C} {Y : C} (r : R) (f : X Y) :
F.map (r f) = r F.map f
@[simp]
theorem CategoryTheory.Functor.map_units_smul {R : Type u_1} [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {X : C} {Y : C} (r : Rˣ) (f : X Y) :
F.map (r f) = r F.map f
instance CategoryTheory.Functor.instLinearId {R : Type u_1} [] {C : Type u_2} [] [] :
Equations
• =
instance CategoryTheory.Functor.instLinearComp {R : Type u_1} [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {E : Type u_4} [] [] (G : ) [G.Additive] :
Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapLinearMap_apply (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {X : C} {Y : C} :
∀ (a : X Y), = (F.mapAddHom).toFun a
def CategoryTheory.Functor.mapLinearMap (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {X : C} {Y : C} :
(X Y) →ₗ[R] F.obj X F.obj Y

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

Equations
• = let __src := F.mapAddHom; { toFun := (__src).toFun, map_add' := , map_smul' := }
Instances For
theorem CategoryTheory.Functor.coe_mapLinearMap (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] [] [] (F : ) [F.Additive] {X : C} {Y : C} :
= F.map
instance CategoryTheory.Functor.inducedFunctorLinear (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] (F : CD) :
Equations
• =
instance CategoryTheory.Functor.fullSubcategoryInclusionLinear (R : Type u_1) [] {C : Type u_2} [] [] (Z : CProp) :
Equations
• =
instance CategoryTheory.Functor.natLinear {C : Type u_2} {D : Type u_3} [] [] (F : ) [F.Additive] :
Equations
• =
instance CategoryTheory.Functor.intLinear {C : Type u_2} {D : Type u_3} [] [] (F : ) [F.Additive] :
Equations
• =
instance CategoryTheory.Functor.ratLinear {C : Type u_2} {D : Type u_3} [] [] (F : ) [F.Additive] :
Equations
• =
instance CategoryTheory.Equivalence.inverseLinear (R : Type u_1) [] {C : Type u_2} {D : Type u_3} [] [] [] [] (e : C D) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] :
Equations
• =