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]
:
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
Instances
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)
:
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)
:
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)
:
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)
:
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.Functor D C)
[F.Monoidal]
[F.Faithful]
[F.Additive]
[CategoryTheory.Functor.Linear R F]
:
A faithful linear monoidal functor to a linear monoidal category ensures that the domain is linear monoidal.