# mathlibdocumentation

category_theory.monoidal.linear

# 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)  :
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} [self : C] {W X Y Z : C} (f : W X) (r : R) (g : Y Z) :
f r g = r (f g)
@[simp]
theorem category_theory.monoidal_linear.smul_tensor {R : Type u_1} [semiring R] {C : Type u_2} [self : C] {W X Y Z : C} (r : R) (f : W X) (g : Y Z) :
r f g = r (f g)
@[protected, instance]
def category_theory.tensor_left_linear (R : Type u_1) [semiring R] (C : Type u_2) (X : C) :
@[protected, instance]
def category_theory.tensor_right_linear (R : Type u_1) [semiring R] (C : Type u_2) (X : C) :
@[protected, instance]
def category_theory.tensoring_left_linear (R : Type u_1) [semiring R] (C : Type u_2) (X : C) :
@[protected, instance]
def category_theory.tensoring_right_linear (R : Type u_1) [semiring R] (C : Type u_2) (X : C) :