RE: Category Theory from RFC Walters' book

[Steve Vickers <s.j.vickers@open.ac.uk>]

> Hello Category Theory community,
>
>      I am rereading RFC Walters' "Categories and Computer Science".
> In chapter 1 Section 3 (starting on pg . 10), Walters discusses the
> the notion of generators and relations to generate categories. He
> gives several examples of this concept. E.g. "Example 15. Consider
> the category presented by one object A, one arrow e:A->A, and the
> one relation e.e.e.e = 1subA. From this, he deduces by hand the
> category has additional arrows e .e, e.e.e. I have two questions:
>
> 1) Walters shows that e.e.e = e is not "deducible". What kind of
>      formal system/inference rule system is "at  work" here that
>      allows us to deduce
>      formally any additional arrows and allows us to deduce
>      arrow relations from the "axiom" relation, i.e. e.e.e.e = 1subA??
>     Is this some kind of equational logic? Please specify in detail.
>
> 2) Given generators and relations are we guaranteed to get a category?

It is folklore that the method of generators and relations works for any
essentially algebraic theory with finitary operators, as well as for some
more general ones. "Algebraic" means defined by operators and equational
laws (could be many-sorted); "essentially" means that the operators may be
partial, with their domains of definition described by finite sets of
equations.

The way the method works is that from the presentation by generators and
relations one can derive a universal property of the desired algebra, so the
problem is whether an algebra does indeed exist with that property. If it
does, then it is unique up to isomorphism.

The theory of categories is essentially algebraic, so generators and
relations for a category do present a category.

I wish I knew of an introductory text describing the techniques at this
level of generality, but unfortunately I'm not aware of any - maybe somebody
can suggest one. Manes's book "Algebraic Theories" is quite good on the
algebraic case.

Here's a sketch of a formal system.

>>>>>>>>>>>>>>>>>>>>>>>>
Terms are of two sorts: object and arrow.

Term formation is by function symbols s, t, i and c, with the obvious
arities, for source, target, identity and composition. (Note at this level
that a term exists for the composite of any two arrows, regardless of
whether they are composable.)

Equality of terms is symmetric and transitive, but _not_ reflexive.

Rules include the following (x and y are objects, f and g are arrows).

  f=g |- s(f)=s(g)
  f=g |- t(f)=t(g)
  x=y |- i(x)=i(y)
  f1=f2, g1=g2, t(f1)=s(g1), t(f2)=s(g2) |- c(f1,g1)=c(f2,g2)

Also rules for the usual equational laws of category theory (associativity
etc.), and

  |- u=u    for each generator u (object or arrow)
  |- r        for each equational relation r

The category is then got by taking all terms z for which z=z, modulo
equality.
<<<<<<<<<<<<<<<<<<

Steve Vickers.