mathlib documentation

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]
  • 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