Prop

definition example

A prop (historically PROP, “products and permutations category”) is a symmetric strict Monoidal Category $(\mathcal{C},0,+)$ with $\mathrm{Ob}(\mathcal{C})=\mathbb{N}$, monoidal unit $0$ and monoidal product on objects given by addition. Every object $n$ is the $n$-fold product of the generating object $1$. To specify a prop it suffices to give

(i) hom-sets $\mathcal{C}(m,n)$ for $m,n\in \mathbb{N}$; (ii) identities ${\mathrm{id}}_n:n\to n$; (iii) symmetries ${\sigma }_{m,n}:m+n\to n+m$; (iv) composition $f;g:m\to p$ for $f:m\to n$, $g:n\to p$; (v) monoidal product $f+g:m+n\to m^{\prime }+n^{\prime }$ for $f:m\to m^{\prime }$, $g:n\to n^{\prime }$,

and check the axioms of a symmetric monoidal category. Props are the complementary simplification of SMCs to symmetric monoidal preorders: preorders constrain the morphisms (at most one), props constrain the objects (generated by $1$). Consequently wiring diagrams for props need no labels on the wires — perfect for signal flow graphs, which have wires of a single type.

Sources: 7 Sketches §5.2 (Definition 5.2, Examples 5.3, 5.6–5.8, 5.12, Definition 5.11, Exercises 5.5, 5.9, 5.10), §5.2.2–5.2.5, §5.3–5.4, §6.5.3; Kittenlab Lecture 4 ($\mathsf{Fin}$ and $\mathsf{Mat}$ with objects $\mathbb{N}$); Catlab @theory / ThBiproductCategory.

Examples

prop	morphisms $m\to n$	notes
$\mathbf{FinSet}$	functions $\underline{m}\to \underline{n}$; $f+g$ by disjoint union (Eq. 5.4)	Example 5.3, 7S Exercise 5.5
$\mathbf{Bij}$	bijections (empty unless $m=n$)	the Free Prop on the empty signature (Example 5.27)
$\mathbf{Corel}$	partitions of $\underline{m}\bigsqcup \underline{n}$	compact closed (Example 5.7)
$\mathbf{Rel}$	relations $R\subseteq \underline{m}\times \underline{n}$	Example 5.8; ${\mathbf{Rel}}_R$ for a rig $R$ (Definition 5.79)
$\mathbf{PG}$	open directed acyclic port graphs	the free prop on one generator of every arity
$\mathrm{Free}(G)$	$G$-labeled port graphs / prop expressions	${\mathbf{SFG}}_R=\mathrm{Free}(G_R)$ (signal flow graphs)
$\mathbf{Mat}(R)$	$m\times n$ matrices over a Rig $R$	composition = matrix multiplication, $+$ = direct sum
${\mathbf{LinRel}}_R$	linear relations $\subseteq R^m\times R^n$	Graphical Linear Algebra
posetal props	a poset structure $⪯$ on $\mathbb{N}$ with $+$ monotone	7S Exercise 5.9: discrete, usual, reverse orders; not divisibility
${\mathbf{Cospan}}_{\mathbf{FinSet}}$	cospans $\underline{m}\to N\leftarrow \underline{n}$	the hypergraph prop (Chapter 6)

Prop functors and presentations

A prop functor $F:\mathcal{C}\to \mathcal{D}$ is a functor that is identity on objects and preserves $+$ on morphisms (Definition 5.11): e.g. $\mathbf{Bij}\hookrightarrow \mathbf{FinSet}$, and $\mathbf{FinSet}\to \mathbf{Rel}$ sending $f$ to its graph $\{(i,f(i))\}$ (Example 5.12). The semantics functor $S:{\mathbf{SFG}}_R\to \mathbf{Mat}(R)$ is the key example (Functorial Semantics). Props are built by free constructions on a signature and by presentations (generators and equations); Theorem 5.60 gives a presentation of $\mathbf{Mat}(R)$. A prop presented by generators $\mu :2\to 1$, $\eta :0\to 1$ and the monoid equations is “the theory of monoids”: monoid objects in $\mathcal{C}$ are strict monoidal functors from it (Remark 5.74) — Lawvere’s algebraic theories.

Props are exactly $\mathbb{N}$-coloured operads’ “one-sorted” cousins; a symmetric strict monoidal category is a commutative Monoid Object in $(\mathbf{Cat},\times ,1)$ (Example 5.71).

JuliaLeanHaskell

Docs: FinSets · Theories & presentations — Kittenlab Lecture 4

using Catlab
# FinSet with + is a prop: objects are natural numbers, morphisms functions, ⊕ is disjoint union
f = FinFunction([1, 1, 2], 2); g = FinFunction([3, 1], 4)
oplus(f, g)                       # f + g : 5 → 6 (Eq. 5.4)
# Catlab's theories of props: ThBiproductCategory (matrices), ThHypergraphCategory, etc.;
# free props via @present on a signature with a single generating object:
@present SigSFG(FreeSymmetricMonoidalCategory) begin
  X::Ob
  copy::Hom(X, X ⊗ X); discard::Hom(X, munit())
  add::Hom(X ⊗ X, X); zero::Hom(munit(), X)
  a::Hom(X, X)                     # one scalar generator (add one per rig element)
end

-- Mathlib has no bundled "prop"; a prop is a strict symmetric monoidal category on ℕ.
-- The skeleton of FinSet (`FintypeCat.Skeleton`) with sums is the prototypical example.
#check CategoryTheory.FintypeCat.Skeleton

-- a prop as a type of morphisms indexed by (m, n) with series and parallel composition
class Prop' hom where
  idP    :: Int -> hom
  compP  :: hom -> hom -> hom        -- f ; g when arities match
  plusP  :: hom -> hom -> hom        -- f + g
  swapP  :: Int -> Int -> hom        -- σ_{m,n}
-- e.g. matrices over a rig (see Prop of Matrices), finite functions (see Category of Finite Sets)