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]
:
- tensor_smul : ∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom f (r • g) = r • CategoryTheory.MonoidalCategory.tensorHom f g
- smul_tensor : ∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom (r • f) g = r • CategoryTheory.MonoidalCategory.tensorHom f g
A category is MonoidalLinear R if tensoring is R-linear in both factors.
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.MonoidalFunctor D C)
[CategoryTheory.Faithful F.toFunctor]
[CategoryTheory.Functor.Additive F.toFunctor]
[CategoryTheory.Functor.Linear R F.toFunctor]
:
A faithful linear monoidal functor to a linear monoidal category ensures that the domain is linear monoidal.