RE: [Axiom-developer] Curiosities with Axiom mathematical structures

[Bill Page]

On March 13, 2006 6:34 AM Ralf Hemmecke asked:
> ... 
> But here the question to our category theory experts:
> Since Monoid is something like (*,1) would it make sense
> to speak of a category (in the mathematical sense) of
> 
>    monoids that have * and 1 as their operations              
>       (1)
> 
> ? Morphisms would respect 1 not just the identity element 
> with respect to *. And for each morphism f we would have
> f(a*b) = f(a)*f(b). Of course as operations the two * above
> are different but in that category they have to have the same
> name. (No idea whether this makes sense, but it seems that
> this is the way as "Category" it is implemented in Axiom/Aldor.)
> 
> Then, of course, (N, +, 0) is not an object in the category 
> given by (1).
> 

I keep trying to answer these questions but I am not sure I
would like to classify myself as an "expert" in category theory.
:) But here goes ...

In category theory **Mon** (** means written in bold face font)
consists of all monoids (as objects) and all monoid homomorphisms
as morphisms. This does not say anything directly about what
operation are present "inside" the objects of the category. It
is one of the goals of category theory to define what we mean
by 'monoid' entirely in terms of the homomorphisms and perhaps
statements about the existence of "special" objects).

It turns out that an individual object of **Mon** is also a
category. It consists of a single object. The morphisms are words.
There is an identity morphism that we can denote '1'. Composition
is just the monoid operation. (N, +, 0) is such an object of
**Mon**.

To make a connection with categories in Axiom, I would want to
say that 'Monoid' represents the category **Mon** while
'Monoid(*$INT,1)' denotes an object of **Mon**. In fact both
of these are categories in their own right.

This brings up a design feature of Axiom and Aldor that I do
not really like. Axiom and Aldor implement a strict two-level
type class hierachy that distinquishes between categories and
domains. Just as in category theory, I think this distinction
is necessary in order to build mathematical constructs. But
categories and domains should not remain strictly separate.
There are many times when we might want to treat a category as
a domain in some other category. We sometimes need to be able
to "flatten" this hierachy and consider really only one kind
of type.

I think this is very closely related to the idea of "reflection"
as discussed some months ago by Peter Broadbery:

http://lists.nongnu.org/archive/html/axiom-developer/2005-09/msg00250.html

When we can treat categories as domains, then domains become
members and we can "ask questions" and manipulate domains (and
categories) as true "first-level" objects.

Regards,
Bill Page.