# Linear monoidal categories #

A monoidal category is MonoidalLinear R if it is monoidal preadditive and tensor product of morphisms is R-linear in both factors.

class CategoryTheory.MonoidalLinear (R : Type u_1) [] (C : Type u_2) [] [] :

A category is MonoidalLinear R if tensoring is R-linear in both factors.

• whiskerLeft_smul : ∀ (X : C) {Y Z : C} (r : R) (f : Y Z),
• smul_whiskerRight : ∀ (r : R) {Y Z : C} (f : Y Z) (X : C),
Instances
@[simp]
theorem CategoryTheory.MonoidalLinear.whiskerLeft_smul {R : Type u_1} [] {C : Type u_2} [] [] [self : ] (X : C) {Y : C} {Z : C} (r : R) (f : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalLinear.smul_whiskerRight {R : Type u_1} [] {C : Type u_2} [] [] [self : ] (r : R) {Y : C} {Z : C} (f : Y Z) (X : C) :
instance CategoryTheory.tensorLeft_linear (R : Type u_1) [] {C : Type u_2} [] [] (X : C) :
Equations
• =
instance CategoryTheory.tensorRight_linear (R : Type u_1) [] {C : Type u_2} [] [] (X : C) :
Equations
• =
instance CategoryTheory.tensoringLeft_linear (R : Type u_1) [] {C : Type u_2} [] [] (X : C) :
Equations
• =
instance CategoryTheory.tensoringRight_linear (R : Type u_1) [] {C : Type u_2} [] [] (X : C) :
Equations
• =
theorem CategoryTheory.monoidalLinearOfFaithful (R : Type u_1) [] {C : Type u_2} [] [] {D : Type u_3} [] [] (F : ) [F.Faithful] [F.Additive] [CategoryTheory.Functor.Linear R F.toFunctor] :

A faithful linear monoidal functor to a linear monoidal category ensures that the domain is linear monoidal.