mathlib documentation


Linear structure on functor categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]

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

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