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 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 of this typeclass
theorem category_theory.tensor_sum {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.monoidal_category C] [category_theory.monoidal_preadditive C] {P Q R S : C} {J : Type u_3} (s : finset J) (f : P Q) (g : J (R S)) :
f s.sum (λ (j : J), g j) = s.sum (λ (j : J), f g j)
theorem category_theory.sum_tensor {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] [category_theory.monoidal_category C] [category_theory.monoidal_preadditive C] {P Q R S : C} {J : Type u_3} (s : finset J) (f : P Q) (g : J (R S)) :
s.sum (λ (j : J), g j) f = s.sum (λ (j : J), g j f)

The isomorphism showing how tensor product on the left distributes over direct sums.

Equations

The isomorphism showing how tensor product on the right distributes over direct sums.

Equations