Linear structure on functor categories

If C and D are categories and D is R-linear, then C ⥤ D is also R-linear.

instance CategoryTheory.functorCategoryLinear {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] : CategoryTheory.Linear R (CategoryTheory.Functor C D)

Equations

• CategoryTheory.functorCategoryLinear = { homModule := fun (F G : CategoryTheory.Functor C D) => Module.mk ⋯ ⋯, smul_comp := ⋯, comp_smul := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.appLinearMap_apply {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) : (CategoryTheory.NatTrans.appLinearMap X) α = α.app X

def CategoryTheory.NatTrans.appLinearMap {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) : (F ⟶ G) →ₗ[R] F.obj X ⟶ G.obj X

Application of a natural transformation at a fixed object, as group homomorphism

Equations

• CategoryTheory.NatTrans.appLinearMap X = { toFun := fun (α : F ⟶ G) => α.app X, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.app_smul {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (r : R) (α : F ⟶ G) : (r • α).app X = r • α.app X