Cartesian monoidal category

In mathematics, specifically in the field known as , a where the monoidal ("tensor") product is the is called a cartesian monoidal category. Any with finite products (a "finite product category") can be thought of as a cartesian monoidal category. In any cartesian monoidal category, the terminal object is the monoidal unit. , a monoidal finite coproduct category with the monoidal structure given by the coproduct and unit the initial object is called a cocartesian monoidal category, and any finite coproduct category can be thought of as a cocartesian monoidal category. Cartesian categories with an internal Hom functor that is an adjoint functor to the product are called . Cartesian monoidal categories have a number of special and important properties, such as the existence of diagonal maps Δx : x → x ⊗ x and augmentations ex : x → I for any x. In applications to computer science we can think of Δ as "duplicating data" and e as "deleting data". These maps make any object into a comonoid. In fact, any object in a cartesian monoidal category becomes a comonoid in a unique way. Cartesian monoidal categories: Set, the with the singleton set serving as the unit. Cat, the with the , where the category with one object and only its identity map is the unit. Cocartesian monoidal categories: Vect, the over a given field, can be made cocartesian monoidal with the monoidal product given by the direct sum of vector spaces and the trivial vector space as unit. Ab, the , with the direct sum of abelian groups as monoidal product and the trivial group as unit. More generally, the category R-Mod of (left) modules over a ring R (commutative or not) becomes a cocartesian monoidal category with the direct sum of modules as tensor product and the trivial module as unit. In each of these categories of modules equipped with a cocartesian monoidal structure, finite products and coproducts coincide (in the sense that the product and coproduct of finitely many objects are isomorphic). Or more formally, if f : X1 ∐ ... ∐ Xn → X1 × ...