sec-toolkit-algebraic-theories
1.5 Algebraic theories, sketches, and generative worlds
A category records which objects and processes exist and how they compose. It need not reveal a small vocabulary from which those objects and processes are generated. Learning a world category and learning its theory of construction are therefore different problems. The second can be much more compact: a few operations and equations may account for indefinitely many composites.
A signature names sorts and primitive operations. An algebraic theory also specifies how those operations may be substituted and which composite expressions are equal. Lawvere expressed a one-sorted finitary algebraic theory as a category \(\mathbb L\) with finite products, generated by a distinguished object \(X\) and its finite powers
A morphism \(X^n\to X^m\) is an abstract \(m\)-tuple of \(n\)-ary operations, composition is substitution, and equality of morphisms records equational laws.
A one-sorted Lawvere theory is a small finite-product category \(\mathbb L\) generated by one object \(X\). A model of \(\mathbb L\) in a category \(\mathcal C\) with finite products is a product-preserving functor
Natural transformations between such functors are homomorphisms of models.
The distinction between theory and model is essential for learning. The theory of groups contains multiplication, unit, inverse, and their equations. A particular group is one model of that theory. Likewise, a learned parameter vector or one encountered physical assembly is a realization, not the generating theory shared across realizations.
A completed category of formal operations is often too large to learn or write down directly. A sketch presents it economically.
A sketch \(\mathbb S\) consists of a graph of generating objects and arrows, specified commutative diagrams, and designated cones or cocones. A model sends this data into a semantic category and preserves the declared equations and universal constructions. Relative to a preservation doctrine \(\mathfrak D\), write
for the category freely completed under the structure demanded by \(\mathfrak D\), modulo the declared relations.
Thus a sketch is neither an informal drawing nor a partial model. It is a finite presentation whose completion generates a theory and whose structure-preserving functors supply its semantics. Finite-product sketches present algebraic theories; finite-limit sketches can also specify typed domains of partially defined operations.
A PROP is a strict symmetric monoidal category whose objects are the natural numbers and whose tensor on objects is addition. A morphism \(m\to n\) represents an operation with \(m\) inputs and \(n\) outputs. An algebra of a PROP \(\mathbb P\) in a symmetric monoidal category \(\mathcal V\) is a symmetric monoidal functor
up to the chosen strictness or coherence convention.
PROPs are useful when juxtaposition is available but copying and deletion are not automatic. They are therefore natural theories of physical construction, circuits, resources, and multi-input/multi-output processes. Lawvere theories and PROPs are neighboring doctrines, not interchangeable names: Cartesian structure freely supplies copying and deletion, while a general symmetric monoidal theory does not.