FOM: organizing; Boolean rings; signature

[Vaughan Pratt]

From: Vaughan Pratt <pratt at CS.Stanford.EDU>
>Steve is convinced category theory will join communism in hell.
		    ^^^^^^^^^^^^^^^

Correction, I should have said category theoretic foundations.

>Naturally Steve views Lawvere theories, monads, and all other "categorical
>dys-foundations" as "incredibly complex."  This should come as no suprise
>to anyone who's read Steve's correspondence with Colin McLarty.

Those familiar with Lawvere theories will know that they are strikingly
simple.  Those not might be interested in the details; I'll describe
only the most special case, namely homogeneous (one sort), with all
arities finite and discrete, and give a few examples.  Paradoxically its
generalizations are even simpler to define, I'll give a couple examples
there as well.

A *finitary homogeneous algebraic theory* in the sense of Lawvere is a
category T having for its objects the natural numbers, such that object n
is the product of n copies of the object 1.  (Names are immaterial here,
and we can make this seem more reasonable by renaming n as X^n where X
is to be viewed as an indeterminate symbol.)

That's the definition.  Whether this is incredibly complex depends on
your feelings about categories and products.

A *set-valued model* of T is a functor from T to Set that preserves
finite products.  (Hence when it maps X to some set, which constitutes
the *carrier* of the model, it must map X^n to the n-th power of that
set.)  A *homomorphism* of two models of the same theory is a natural
transformation between them.

--------------------------

Example 1: the empty signature.  Take the theory T to be skel(FinSet)^op,
the opposite of the skeletal category of finite sets and functions
between them.  (Skeletal means that all isomorphisms are automorphisms,
i.e. no two distinct objects are isomorphic.  Thus we have one object
per natural number, as required.)

If skel and op are uncomfortable notions, we may equivalently define the
morphisms f:m->n to be all functions F:{0,1,...,n-1} -> {0,1,...,m-1}.
(There are m^n of these.)  Composition of morphisms is defined oppositely
to composition of their representing functions.  Thus

		   f      g
		m ---> n ---> p

is the morphism represented by the function FG from p to m defined by
(FG)(x) = F(G(x)) for all x in {0,1,...,p-1}.

Each such morphism f:m->n, represented by the function
F:{0,...,n-1}->{0,...,m-1}, can be understood as the lambda term

	\lambda x_0 ... x_{m-1} . x_{F(0)} x_{F(1)} ... x_{F(n-1)}

This term takes a list of m items as arguments and returns a list of
n items.

The n projections from n to 1 are the n lambda terms of the form

	\lambda x_0 ... x_{n-1} . x_i

for some i such that 0 <= i < n.  In general the morphisms of T from m
to n may be understood as n-tuples of projections from n.

A model of T is a functor from T to Set that sends {0} to an arbitrary
set, all other objects to finite powers of that set, and the morphisms to
tuples of projections of those powers.  Hence there is one model per set.
The natural transformations between two such models consists of exactly
the functions between their corresponding carriers.  Thus the theory
with the empty signature is just the equational theory of pure sets.

--------------------------

Example 2: the theory of Boolean algebras.  Represent object n as the
n-th power of the set {0,1}, and take the morphisms to be all functions
between those sets.

If we count the morphisms from 2 (= {0,1}^2) to 1 (= {0,1}^1) we find
there are 2^4 = 16 of them.  These represent the 16 binary Boolean
operations.  In general there are 2^2^n n-ary Boolean operations, as
expected.

The equational theory of Boolean algebras resides in the commuting
diagrams of T.  Functors preserve commuting diagrams whence the models
of T satisfy all the laws of Boolean algebra.

For example distributivity, (x v y) & z = x&z v y&z, is expressed by
the following square.

                   (xvy,z)
		3 --------> 2
		|           |
		|           |
    (x&z,y&z)	|           | &
		|           |
		V     v     V
		2 --------> 1

Here each of (xvy,z) and (x&z,y&z) is a pair of ternary Boolean
operations, while & and v are single binary Boolean operations.

--------------------------

Example 3: the theory of commutative rings with unit.  Take the morphisms
from m to n to consist of all n-tuples of polynomials in m variables
with integer coefficients.  Some thought and comparison with the ideas
in example 2 shows that the product-preserving functors from T to Set
are exactly the commutative rings with unit, with 1 being mapped to the
carrier of the ring.  The natural transformations of these functors are
the unit-preserving ring homomorphisms.

--------------------------

Example 4: simplicial sets.  (This is more general than an algebraic
theory because we drop the requirement that the objects be powers of 1.)
Take the objects of T to be the finite chains (linearly ordered sets)
and the morphisms to be the opposite (reversal) of the monotone functions
between those chains.

The idea is that the objects are types, one type per dimension, and
the inequalities in a chain model the edges of a simplex.  For example
the six inequalities in the four-element chain model the six edges of
the tetrahedron.  A simplicial set is a set of simplexes of various
dimensions, some of which share faces or even are faces of others.

A functor from T to Set (which now need not preserve products) assigns
to each n a set of elements which can be understood as n-dimensional
simplices.  The morphisms from n-1 to n reverse to become the functions
which, given a simplex, return one of its faces.  The morphisms from
n-2 to n do the same but drop down two dimensions.  Note that there are
nontrivial commutavities to be respected when dropping two dimensions,
which the theory represents faithfully.

--------------------------

Example 5: cubical sets.  Same as 4 except that manifolds decompose as
n-cubes rather than n-simplexes.  Take T to be the finite bipointed sets
(equivalently, algebras with signature B,E, i.e. two constants denoting
Beginning and End), one such bipointed set per cardinality, and the
morphisms of T to be all functions between them that preserve both
constants: f(B)=B, f(E)=E.  (No need to reverse T in this construction!)

A cubical set is a functor from T to Set.  The three-element object
(two elements of which are constants) is sent by the functor to the set
of all 1-cubes (edges).  The four-element object is sent to the set of
all 2-cubes (squares), and so on.

One law that holds of cubical sets is that if you apply say the north
and east functions to a square to get its north and east edges, and
then take the appropriate endpoint of each of those edges, those two
endpoints will be equal, being where those edges meet.  So we would hope
to find that law in T.  And we do.  The following diagram

		   1/B
	{B,0,1,E} -----> {B,0,E}
	    |               |
	    |               |
    0/B,1/0 |               | 0/B
	    |               |
	    V               V
	  {B,0,E} -----> {B,E}
	           0/B

(where 1/B means 1 is sent to B) evidently commutes.  Its image under
an arbitrary functor from T to Set denoting a cubical set is a commuting
square in the theory of that cubical set describing the above-mentioned
desired commutativity.

--------------------------

Example 6.  Locomotives.  Take T to have seven objects: 6 for the 6
wheels and one for the locomotive as a whole.  Take the morphisms of
T to be one morphism from each wheel to the locomotive.  (Think of
wheels and locomotives as sets of atoms, and think of the morphisms
as functions mapping each atom of the given wheel to the corresponding
atom of the locomotive as a whole, i.e. an injection.)  Then a functor
from T^op to Set denotes a set of locomotives and six sets of wheels.
Each of the six morphisms is mapped by the functor to a function which,
given a locomotive, gives back one of the wheels.

In some models the same wheel will be used as more than one of the six
wheels, but this is equational logic which has no way of avoiding such
screwy models!  They can be avoided by introducing ad hoc restrictions
on the functors, but this is no longer pure equational logic.

This example has no nontrivial commutativities.  However if we extend
to have 10 spokes per wheel, so that T now has 1+6+6*10 = 67 objects,
and put in the necessary morphisms as functions mapping atoms of spokes
to atoms of wheels (of which the spokes are a part), then we might hope
for some commutativities.  But in fact we don't get any because wheels
aren't supposed to share spokes.  Contrast this with adjacent edges of
a square, which do share a boundary point and therefore do have
nontrivial equations in the theory.

Obviously more elaborate theories of locomotives will start to introduce
nontrivial equations, wherever one has multiple ways of getting between
two parts of our theoretical locomotive.

Vaughan Pratt