mathlib3 documentation

category_theory.monoidal.linear

Linear monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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