mathlib documentation

category_theory.linear.functor_category

Linear structure on functor categories #

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

@[protected, instance]
Equations

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

Equations
@[simp]
theorem category_theory.nat_trans.app_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 D] [category_theory.linear R D] {F G : C D} (X : C) (r : R) (α : F G) :
(r α).app X = r α.app X