FOM: Definition of Lawvere theory: additional condition needed

[Vaughan Pratt]

It occurs to me that there is an incompleteness in my noncategorical
formulation of Lawvere theory, namely as a graph together with a
congruence on its paths, as described in post 387 in the FOM archives
for March,

	http://www.math.psu.edu/simpson/fom/postings/9803.html

My formulation suffers from the same degeneracy (basis dependence) as
does the signature-based definition of an equational theory.  The standard
categorical definition of Lawvere theory does not have this degeneracy.

Fortunately my formulation is easily brought into correspondence with
Lawvere's basis-independent one by adding the following condition.

*** Every path is congruent to exactly one edge. ***

(An edge is of course a path of length one.  Edges are the Lawvere
counterpart of operation symbols, paths are the counterpart of terms,
and path concatenation is the counterpart of composition of terms.)

With this condition an equivalence (bijection up to isomorphism) can be
exhibited between these two frameworks for Lawvere theories.  To convert
a graph-based theory to a category-based one, note that the paths form
the morphisms of a category whose objects are the vertices and whose
composition is concatenation.  The quotient modulo the congruence is
then the Lawvere theory.

Conversely to convert a category to a graph G and a congruence on
the paths of G, take the vertices of G to be the objects, the edges
of G to be the morphisms, and the congruence on paths in G to be the
commuting diagrams in the category.  (The commuting diagrams of a
category constitute the equational representation of that category in
terms of its paths.  This representation corresponds to the canonical
generator-relator representation of a group G as the free group generated
by the elements of G modulo all identities holding in G.)

The graphs produced by the latter conversion meet my proposed condition.
Furthermore applying the first conversion to graphs arising from the
second conversion gets you back to a category isomorphic to the one
started from.  And conversely applying the second conversion to the
result of the first gets you back to a graph-congruence pair isomorphic
to the starting one.

The two "isomorphic to"'s here are responsible for this only being
an equivalence of frameworks, had they been "equal to" we would have
established an isomorphism (structure-preserving bijection) of frameworks.

Without the above condition however we don't even get an equivalence,
there is a genuine degeneracy in the graph-based definition.

The difference between graph theory and category theory is that category
theory incorporates the congruence on paths as part of its structure,
permitting every instance of "congruent to" to be streamlined to
"equal to".  The graph theory formulation of category theory is like a
bicycle with training wheels: great for getting started but eventually
you want to take off the training wheels so you can go faster.

Vaughan Pratt