ifc-0009
0.6 Algebraic theories, sketches, and models
A signature lists operation symbols. An algebraic theory also records how operations compose and which equations they satisfy. Lawvere expressed a one-sorted algebraic theory as a category \(\mathbb T\) with finite products, generated by a distinguished object and its finite powers [ Lawvere , 1963 ] . A model in a category \(\mathcal C\) with finite products is a product-preserving functor
For the theory of monoids, the presentation contains multiplication \(\mu :X\times X\to X\), a unit \(e:1\to X\), and the associative and unit equations. A model in \(\mathsf{Set}\) is an ordinary monoid. A model in another suitable category interprets the same formal theory there. Theory and model must not be conflated: a parameter vector is one realization, not the compositional specification shared across realizations.
A completed theory can be large. A sketch presents one compactly by a graph of generating objects and arrows, declared commutative diagrams, and designated cones or cocones [ Ehresmann , 1968 , Barr and Wells , 1999 ] . A model maps the presentation to a semantic category and preserves the specified structure.
A candidate presentation extension is a typed map of presentations
together with an interpretation of the new generators and relations. The map records how the old language is intended to transport into the proposed one. It is the presentation-changing component of a candidate package comparison, not by itself an admitted theory extension.
Restriction along \(J\) sends an expanded model back to its old visible part:
The fiber over an old model records its possible expansions. A unique expansion may merely name structure that was already determined. Several inequivalent expansions expose a genuinely new choice. No expansion means that the new theory rejects or must reinterpret that old model.
This gives the book a concrete target for transformational creativity: propose not only a sentence, but an augmented presentation whose models, transport, and new consequences can be examined. Chapter 2 adds the finite-realization and independent-admission conditions under which such a proposal earns an unqualified theory-extension status.