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.{u_3, 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.{u_3, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
(X : C)
:
instance
CategoryTheory.tensorRight_linear
(R : Type u_1)
[Semiring R]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
(X : C)
:
instance
CategoryTheory.tensoringLeft_linear
(R : Type u_1)
[Semiring R]
{C : Type u_2}
[Category.{u_3, 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.{u_3, 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.{u_5, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
{D : Type u_3}
[Category.{u_4, 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.
@[deprecated CategoryTheory.MonoidalLinear.ofFaithful (since := "2025-10-17")]
theorem
CategoryTheory.monoidalLinearOfFaithful
(R : Type u_1)
[Semiring R]
{C : Type u_2}
[Category.{u_5, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
{D : Type u_3}
[Category.{u_4, 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
Alias of CategoryTheory.MonoidalLinear.ofFaithful.
A faithful linear monoidal functor to a linear monoidal category ensures that the domain is linear monoidal.