mathlib documentation

category_theory.monoidal.preadditive

Preadditive monoidal categories #

A monoidal category is monoidal_preadditive if it is preadditive and tensor product of morphisms is linear in both factors.

@[class]
  • tensor_zero' : (∀ {W X Y Z : C} (f : W X), f 0 = 0) . "obviously"
  • zero_tensor' : (∀ {W X Y Z : C} (f : Y Z), 0 f = 0) . "obviously"
  • tensor_add' : (∀ {W X Y Z : C} (f : W X) (g h : Y Z), f (g + h) = f g + (f h)) . "obviously"
  • add_tensor' : (∀ {W X Y Z : C} (f g : W X) (h : Y Z), f + g h = f h + (g h)) . "obviously"

A category is monoidal_preadditive if tensoring is linear in both factors.

Note we don't extend preadditive C here, as abelian C already extends it, and we'll need to have both typeclasses sometimes.