Preadditive monoidal categories #
A monoidal category is MonoidalPreadditive
if it is preadditive and tensor product of morphisms
is linear in both factors.
- tensor_zero : ∀ {W X Y Z : C} (f : W ⟶ X), CategoryTheory.MonoidalCategory.tensorHom f 0 = 0
tensoring on the right with a zero morphism gives zero
- zero_tensor : ∀ {W X Y Z : C} (f : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom 0 f = 0
tensoring on the left with a zero morphism gives zero
- tensor_add : ∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom f (g + h) = CategoryTheory.MonoidalCategory.tensorHom f g + CategoryTheory.MonoidalCategory.tensorHom f h
left tensoring with a morphism is compatible with addition
- add_tensor : ∀ {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z), CategoryTheory.MonoidalCategory.tensorHom (f + g) h = CategoryTheory.MonoidalCategory.tensorHom f h + CategoryTheory.MonoidalCategory.tensorHom g h
right tensoring with a morphism is compatible with addition
A category is MonoidalPreadditive
if tensoring is additive 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.
Instances
A faithful additive monoidal functor to a monoidal preadditive category ensures that the domain is monoidal preadditive.
The isomorphism showing how tensor product on the left distributes over direct sums.
Instances For
The isomorphism showing how tensor product on the right distributes over direct sums.