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]
:
@[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)
:
Application of a natural transformation at a fixed object, as group homomorphism
Instances For
@[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)
: