Documentation

Mathlib.CategoryTheory.Monoidal.Linear

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) [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [MonoidalCategory C] [MonoidalPreadditive C] :

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

Instances

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

Functor.Linear R (MonoidalCategory.tensorLeft X)

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

Functor.Linear R (MonoidalCategory.tensorRight X)

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

Functor.Linear R ((MonoidalCategory.tensoringLeft C).obj X)

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

Functor.Linear R ((MonoidalCategory.tensoringRight C).obj X)

theorem CategoryTheory.MonoidalLinear.ofFaithful (R : Type u_1) [Semiring R] {C : Type u_2} [Category.{v_1, u_2} C] [Preadditive C] [Linear R C] [MonoidalCategory C] [MonoidalPreadditive C] [MonoidalLinear R C] {D : Type u_3} [Category.{v_2, u_3} D] [Preadditive D] [Linear R D] [MonoidalCategory D] [MonoidalPreadditive D] (F : Functor D C) [F.Monoidal] [F.Faithful] [Functor.Linear R F] :

MonoidalLinear R D

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