Closed braided preadditive categories are monoidal preadditive #
In a closed braided monoidal category, tensoring on either side with a fixed object is a left
adjoint, so it preserves binary coproducts. In a preadditive category, binary coproducts are
binary biproducts, and a functor preserving them is additive. Hence the tensor product of
morphisms is additive in each variable: the category is MonoidalPreadditive.
This applies to categories such as sheaves of modules, whose monoidal structure is constructed abstractly (for instance by localization) rather than from a bilinear formula on morphisms.
Main declaration #
theorem
TauCeti.monoidalPreadditive_of_monoidalClosed
(D : Type u_1)
[CategoryTheory.Category.{v_1, u_1} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryCoproducts D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
[CategoryTheory.MonoidalClosed D]
:
A closed braided monoidal category which is preadditive with binary coproducts is monoidal preadditive: whiskering on either side is additive.