Linear monoidal categories #
A monoidal category is monoidal_linear R
if it is monoidal preadditive and
tensor product of morphisms is R
-linear in both factors.
@[class]
structure
category_theory.monoidal_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C] :
Type
- tensor_smul' : (∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)) . "obviously"
- smul_tensor' : (∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)) . "obviously"
A category is monoidal_linear R
if tensoring is R
-linear in both factors.
Instances of this typeclass
Instances of other typeclasses for category_theory.monoidal_linear
- category_theory.monoidal_linear.has_sizeof_inst
@[simp]
theorem
category_theory.monoidal_linear.tensor_smul
{R : Type u_1}
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[self : category_theory.monoidal_linear R C]
{W X Y Z : C}
(f : W ⟶ X)
(r : R)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.monoidal_linear.smul_tensor
{R : Type u_1}
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[self : category_theory.monoidal_linear R C]
{W X Y Z : C}
(r : R)
(f : W ⟶ X)
(g : Y ⟶ Z) :
@[protected, instance]
def
category_theory.tensor_left_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensor_right_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_left_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_right_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :