Monoidal Category

definition example theorem

A symmetric monoidal structure on a Category $\mathcal{C}$ consists of

(i) an object $I\in \mathrm{Ob}(\mathcal{C})$, the monoidal unit, and (ii) a Functor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, the monoidal product (a Bifunctor: $f\otimes g$ for morphisms too),

together with well-behaved natural isomorphisms

(a) left unitor ${\lambda }_c:I\otimes c\cong c$, (b) right unitor ${\rho }_c:c\otimes I\cong c$, (c) associator ${\alpha }_{c,d,e}:(c\otimes d)\otimes e\cong c\otimes (d\otimes e)$, (d) swap (braiding, symmetry) ${\sigma }_{c,d}:c\otimes d\cong d\otimes c$ with $\sigma \circ \sigma =\mathrm{id}$,

satisfying coherence laws (the pentagon and triangle equations, hidden under “well behaved” in 7 Sketches’ Rough Definition 4.45). Without (d) one has a monoidal category; a symmetric monoidal category (SMC) has all four. If (a)–(c) are equalities the structure is strict; by Mac Lane’s coherence theorem every monoidal category is equivalent to a strict one (Remark 4.46–4.47: “a symmetric monoidal category is a category equipped with an equivalence to a symmetric strict monoidal category”), so one may pretend strictness — as wiring diagrams implicitly do.

Sources: 7 Sketches §4.4.3 (Definition 4.45, Remarks 4.46–4.47, Examples 4.49, Exercises 4.48, 4.50), §4.4.4, §5–6; DaoFP §4.4 (“Symmetric Monoidal Category” from sums), §5.3 (“Monoidal Category”, “Monoids”), §14.9 (monoidal functors), §15.1 (string diagrams), §17.7 (Day Convolution), §19.1, §20.1 (enrichment); Kittenlab (implicitly: $\mathbf{FinSet}$ with $+$).

A Symmetric Monoidal Preorder is exactly a symmetric monoidal category with at most one morphism between any two objects (7S Exercise 4.48) — monoidal categories are the categorification of monoidal preorders: equations become isomorphisms (“bookkeeping”) which in turn must satisfy new equations.

Examples

category	$\otimes$	$I$	notes
$\mathbf{Set}$	$\times$ (cartesian product; $f\times g$ pointwise)	$\{1\}$	Example 4.49; $\alpha :(s,(t,u))\mapsto ((s,t),u)$; a Cartesian Category
$\mathbf{Set}$, $\mathbf{FinSet}$	$\bigsqcup$ / $+$	$\varnothing$	cocartesian (DaoFP §4.4: $0+a\cong a$, commutativity, associativity, functoriality); the Prop $\mathbf{FinSet}$
any category with finite products / coproducts	$\times$ / $+$	$1$ / $0$	DaoFP Chapters 4–5; “tuple arithmetic”
${\mathbf{Vect}}_k$	${\otimes }_k$	$k$	not cartesian: no diagonal $V\to V\otimes V$ — no copying (quantum)
$[\mathcal{C},\mathcal{C}]$ endofunctors	$\circ$	$\mathrm{Id}$	strict, not symmetric; its monoids are monads (DaoFP §14.7)
$\mathbf{Cat}$	$\times$	$\underline{1}$	cartesian closed (DaoFP §10.1)
${\mathbf{Prof}}_{\mathcal{V}}$ / $\mathbf{Feas}$	product of $\mathcal{V}$-categories	$1$	compact closed (Theorem 4.63)
$\mathbf{Corel}$, ${\mathbf{Cosp}}_{\mathcal{C}}$	$\bigsqcup$	$\varnothing$	compact closed / hypergraph (Chapter 6)
Props, $\mathbf{Mat}(R)$	$+$ on $\mathbb{N}$	$0$	strict SMCs with $\mathrm{Ob}=\mathbb{N}$ (Chapter 5)
$[\mathcal{C},\mathbf{Set}]$	Day Convolution	$\mathcal{C}(I,-)$	DaoFP §17.7

Wiring diagrams and interpretation

An SMC is “an algebraic structure with labelled boxes having multiple typed inputs and outputs” (§4.4.2); series composition is $;$, parallel composition is $\otimes$, crossing wires is $\sigma$, and coherence lets diagrams be read unambiguously (Wiring Diagram, String Diagram). 7S Exercise 4.50 evaluates a diagram of functions in $(\mathbf{Set},1,\times )$ as a single function $A\times B\to G\times F$. DaoFP: “if we think of morphisms as actions, their tensor product corresponds to performing two actions in parallel”, and “a tensor product is the lowest common denominator of product and sum: it has an introduction rule requiring both objects but no elimination rule — once created it forgets how it was created; unlike a cartesian product it has no projections”. Copying and discarding are extra structure (cartesian = every object a cocommutative comonoid).

Structures on / in monoidal categories

• Monoids in a monoidal category ($\mu :m\otimes m\to m$, $\eta :I\to m$, DaoFP §5.3, 7 Sketches §5.4.2), comonoids, Frobenius monoids (§6.3.1), bialgebras.
• Monoidal functors (lax/strong/strict; Definition 6.68, DaoFP §14.9), monoidal natural transformations.
• Enrichment in an SMC (Rough Definition 4.51): hom-objects $\mathcal{X}(x,y)\in \mathcal{V}$, identity ${\mathrm{id}}_x:I\to \mathcal{X}(x,x)$, composition $\mathcal{X}(x,y)\otimes \mathcal{X}(y,z)\to \mathcal{X}(x,z)$; $\mathbf{Set}$-categories are categories (7S Exercise 4.52), $\mathbf{Cost}$-categories have identity elements $0\ge d(x,x)$ (7S Exercise 4.54).
• Closed structures: Monoidal Closed Category ($[c,d]$ with $\mathcal{C}(b\otimes c,d)\cong \mathcal{C}(b,[c,d])$), Compact Closed Category (duals), Cartesian Closed Category; Hypergraph Category; traced categories.
• Operads arise from SMCs by taking multi-input morphisms (§6.5.2).

JuliaLeanHaskell

Docs: FinSets · Theories & presentations · Vignette: SMCs

# Catlab: the GAT of symmetric monoidal categories and free SMC expressions
using Catlab
@present P(FreeSymmetricMonoidalCategory) begin
  (A, B, C)::Ob
  f::Hom(A, B); g::Hom(B ⊗ C, C)
end
f, g = P[:f], P[:g]
(f ⊗ id(P[:C])) ⋅ g                   # series and parallel composition: A ⊗ C → C
braid(P[:A], P[:B])                   # the swap σ_{A,B}
munit(FreeSymmetricMonoidalCategory.Ob)   # I
 
# FinSet with + is a symmetric monoidal category (a prop):
f = FinFunction([2, 1], 2); g = FinFunction([1, 1, 3], 3)
oplus(f, g)                           # f ⊕ g : 5 → 5
# and with ×:
otimes(f, g)                          # f × g : 6 → 6

#check CategoryTheory.MonoidalCategory     -- class: tensorObj, whiskerLeft/Right, tensorUnit, associator, unitors, pentagon, triangle
#check CategoryTheory.SymmetricCategory    -- braiding with symmetry
#check CategoryTheory.BraidedCategory
example : CategoryTheory.MonoidalCategory (Type u) := inferInstance   -- (Type, ×, PUnit)
#check CategoryTheory.MonoidalCategory.associator
#check CategoryTheory.MonoidalCategory.pentagon

-- DaoFP §5.3: Hask with (,) and () is symmetric monoidal (up to isomorphism)
assoc :: ((a, b), c) -> (a, (b, c))
assoc ((a, b), c) = (a, (b, c))
lunit :: ((), a) -> a
lunit ((), a) = a
runit :: (a, ()) -> a
runit (a, ()) = a
swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)
-- functoriality of the tensor: f ⊗ g
tensor :: (a -> a') -> (b -> b') -> (a, b) -> (a', b')
tensor f g (a, b) = (f a, g b)
-- Either / Void give a second symmetric monoidal structure