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

@[simp]

theorem CategoryTheory.MonoidalLinear.whiskerLeft_smul {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] [self : CategoryTheory.MonoidalLinear R C] (X : C) {Y : C} {Z : C} (r : R) (f : Y ⟶ Z) : CategoryTheory.MonoidalCategory.whiskerLeft X (r • f) = r • CategoryTheory.MonoidalCategory.whiskerLeft X f

@[simp]

theorem CategoryTheory.MonoidalLinear.smul_whiskerRight {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] [self : CategoryTheory.MonoidalLinear R C] (r : R) {Y : C} {Z : C} (f : Y ⟶ Z) (X : C) : CategoryTheory.MonoidalCategory.whiskerRight (r • f) X = r • CategoryTheory.MonoidalCategory.whiskerRight f 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

• ⋯ = ⋯

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

• ⋯ = ⋯

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).obj X)

Equations

• ⋯ = ⋯

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).obj X)

Equations

• ⋯ = ⋯

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) [F.Faithful] [F.Additive] [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.