axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] Curiosities with Axiom mathematical structures

 From: Ralf Hemmecke Subject: Re: [Axiom-developer] Curiosities with Axiom mathematical structures Date: Tue, 14 Mar 2006 18:30:11 +0100 User-agent: Thunderbird 1.5 (X11/20051201)

On 03/14/2006 05:28 PM, Page, Bill wrote:

Ralf,
On Tuesday, March 14, 2006 9:56 AM you wrote:

On 03/14/2006 01:43 AM, Gabriel Dos Reis wrote:

"Bill Page" <address@hidden> writes:

| I agree with Martin. One should interpret:

| | if Integer has Monoid(*,1) | | as the question of whether F = (*,1) is a functor from | the category containing Integer to Monoid, the category
| of monoids.

100% agreed.

But that looks like strange syntax to me. If I want to ask

F(Integer) \in Ob(Monoid)


and I have to write "Integer has Monoid(*,1)" that does not really look natural to me.


Category theorists purist do not like to write set membership
because it implies that categories are always sets.



OK. Monoid is a category, but I must be able to tell whether something is an object of that category. I never said that Ob(Monoid) is a set. I did not even claim that it is a class. My "\in" notation just tried to be "intuitive". I know that some people found mathematics on category theory an not set theory.


They prefer to posit the existence of a functor.


Could you be more precise?


But you are right, describing the functor this way does not seem

> very "natural" in Aldor syntax.


What if we say:

Monoid(Integer,*,1)

denotes the particular object in Monoid (since this is what
we have to write in Aldor anyway).



He? If you say "Monoid(Integer,*,1)" is "the particular object in Monoid" then why would I have to write

Integer has Monoid(Integer, *, 1) ?


That also looks unnatural. What would be the meaning of "has" and what should be the types of its first and second argument?

> Then the functor F maps

Integer into Monoid(Integer,*,1):

Integer |-> Monoid(Integer,*,1)


It's hard to follow you. Let me tell you what I understood.


1) There is a category Monoid whose objects are categories. (In that sense Monoid would be on the same type level as "Category" in Aldor.) I order to avoid confusion, lets call it MONOID.

2) Monoid(Integer, *, 1) would be a category.
I hope you _don't_ mean the category structure that comes from
the fact that any monoid can be considered as a category.
But than I cannot interpret what the objects and arrows in that
category would be.


3) For me "Monoid(Integer,*,1)" looks more like the universal algebra given by the carrier set {0,1,-1,...} and operations * and 1 together with the monoid axioms. The axioms are hidden in your notation by the "tag" or predicate (well, it's not a predicate since you want the result type to be a category) "Monoid".


4) If "Monoid(Integer,*,1)" just means: take the (aldor) category that Integer is currently in and forget anything except * and 1, than that looks similar to one of my previous mails where I tried to model F by "MonoidStructure". It is only that I work on the left hand side of "has" and you on the right hand side. But also my suggestion would be "type satisfaction in the sense of Aldor" (if it worked).

> Then:


Integer has Monoid(Integer,*,1)

Looks "natural" since this depends a the Aldor category
containment relation rather than an element-of relation. I.e.
the Aldor category 'Monoid(Integer,*,1)' is a sub-category
of the Aldor category containing Integer. This is just the
concept of type satisfaction in Aldor.


What would be different to

Integer has with {*:(%,%)->%;1:%}

?? Only that "Monoid" appears?

Ralf