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) [Semiring R] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : Prop

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), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (r • f) = r • CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f
• smul_whiskerRight : ∀ (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C), CategoryTheory.MonoidalCategory.tensorHom (r • f) (CategoryTheory.CategoryStruct.id X) = r • CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X)

instance CategoryTheory.tensorLeft_linear (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorLeft X)

Equations

• (_ : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorLeft X)) = (_ : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorLeft X))

instance CategoryTheory.tensorRight_linear (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorRight X)

Equations

• (_ : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorRight X)) = (_ : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorRight X))

instance CategoryTheory.tensoringLeft_linear (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringLeft C).toPrefunctor.obj X)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.tensoringRight_linear (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringRight C).toPrefunctor.obj X)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.monoidalLinearOfFaithful (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] (F : CategoryTheory.MonoidalFunctor D C) [CategoryTheory.Faithful F.toFunctor] [CategoryTheory.Functor.Additive F.toFunctor] [CategoryTheory.Functor.Linear R F.toFunctor] : CategoryTheory.MonoidalLinear R D

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