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]
def
category_theory.functor_category_linear
{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] :
category_theory.linear R (C ⥤ D)
Equations
- category_theory.functor_category_linear = {hom_module := λ (F G : C ⥤ D), {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (r : R) (α : F ⟶ G), {app := λ (X : C), r • α.app X, naturality' := _}}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}, smul_comp' := _, comp_smul' := _}
@[simp]
theorem
category_theory.nat_trans.app_linear_map_apply
{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)
(α : F ⟶ G) :
⇑(category_theory.nat_trans.app_linear_map X) α = α.app X
def
category_theory.nat_trans.app_linear_map
{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) :
Application of a natural transformation at a fixed object, as group homomorphism
@[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) :