Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: The Monoid Category in DC Proof
Replies: 7   Last Post: Nov 11, 2012 10:37 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 2,254
Registered: 7/9/08
Re: The Monoid Category in DC Proof
Posted: Nov 10, 2012 1:17 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Nov 9, 2:34 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Nov 9, 2:11 pm, Rotwang <sg...@hotmail.co.uk> wrote:
>
>
>
>
>
>
>
>
>

> > On 09/11/2012 15:43, Dan Christensen wrote:
>
> > > What is a category?
>
> > > Use the imagery of a directed graph, we can define a category as a
> > > logical structure that satisfies the following axioms (in my DC Proof
> > > notation):

>
> > > 1. ALL(f):[f @ arrows => source(f) @ nodes]
>
> > > where:
> > > @ = epsilon (set/class membership)
> > > arrows is a class
> > > nodes is a class
> > > source(f) is the source node for arrow f

>
> > > 2. ALL(f):[f @ arrows => target(f) @ nodes]
>
> > > where:
> > > target(f) is the target node of arrow f

>
> > > 3. ALL(f):ALL(g):[f @ arrows & g @ arrows
> > >      => [target(f)=source(g) => comp(f,g) @ arrows]]

>
> > > where:
> > > comp(f,g) is the composition of arrow f followed by and arrow g

>
> > > Note the order of arguments -- a minor departure from the usual
> > > presentation. In a graphical sense, the comp(f,g) operator is similar
> > > to the addition of vectors with the head of arrow f being place at the
> > > tail of arrow g.

>
> > > 4. ALL(f):ALL(g):[f @ arrows & g @ arrows
> > >      => [target(f)=source(g)
> > >      => source(comp(f,g))=source(f) & target(comp(f,g))=target(g)]]

>
> > > The source and target of the composition of two arrows must be
> > > compatible with the the targets and sources of those two arrows.

>
> > > 5. ALL(f):ALL(g):ALL(h):[f @ arrows & g @ arrows & h @ arrows
> > >      => [target(f)=source(g) & target(g)=source(h)
> > >      => comp(comp(f,g),h)=comp(f,comp(g,h))]]

>
> > > Composition of arrows is associative.
>
> > > 6, ALL(a):ALL(b):[a @ nodes & b @ nodes
> > >      => ALL(f):[f @ arrows(a,b) <=> f @ arrows & source(f)=a &
> > > target(f)=b]]

>
> > > where:
> > > arrows(a,b) is the class of arrows with source a and target b

>
> > > Although this construction is not referred to by other axioms here,
> > > traditionally, it is part of the definition of a category. It may be
> > > referred to in other definitions and theorems of category theory.

>
> > > 7. ALL(a):[a @ nodes => id(a) @ arrows]
>
> > > where:
> > > id(a) is the identity arrow for node a

>
> > > 8. ALL(f):[f @ arrows => ALL(a):[a @ nodes => [source(f)=a =>
> > > comp(id(a),f)=f]]]

>
> > > 9. ALL(f):[f @ arrows => ALL(a):[a @ nodes => [target(f)=a =>
> > > comp(f,id(a))=f]]]

>
> > This looks OK, though I don't see why you use the terms node, source and
> > target instead of the usual object, dom and cod.

>
> For readability.
>

> > Also you have nothing
> > that says that source and target are only defined on the class of nodes

>
> Not necessary. I only refer to source and target of things known to be
> nodes.
>

> > and that comp(f, g) are only defined for f, g @ arrows with source(g) =
> > target(f). I don't know whether that matters for your intended applications.

>
> Similar argument.
>
>
>
>
>
>
>
>
>
>
>

> > > What is a monoid?
>
> > > The monoid (m,+) is an algebraic structure on a set m that satisfies
> > > the following axioms:

>
> > > 1. 0 @ m
>
> > > 2.  ALL(a):ALL(b):[a @ m & b @ m => a+b @ m]
>
> > > where:
> > > + is a binary operator on m

>
> > > 3. ALL(a):[a @ m => a+0=a & 0+a=a]
>
> > > 0 is the identity element in m with respect to +
>
> > > 4. ALL(a):ALL(b):ALL(c):[a @ m & b @ m & c @ m => a+b+c=a+(b+c)]
>
> > Should that be                                     ^(a+b)+c?
>
> > > + is associative
>
> > This looks fine too (though it's unusual IME to use the + sign to denote
> > the product in a not-necessarily-Abelian monoid).

>
> OK.
>

> > What's below also looks correct to me, but it's way more complicated
> > than it needs to be.
> > You still seem to be stuck on thinking of arrows in
> > a category as functions,

>
> No, they are just arrows. In the case of the monoid, they are
> functions, but, in general, they don't have to be.
>

> > but the category corresponding to a monoid is
> > easier to define if they aren't. Firstly, the unique node doesn't have
> > to be the underlying set m; it can be anything, even an urelement. More
> > importantly, though, you've defined a category whose arrows are the
> > right actions of elements of m on m, and whose composition is given by
> > function composition. But you could just as well have defined the arrows
> > to be the elements of m, and defined composition to be given by +. That is,

>
> > nodes(C) = {*}   /* where * is anything at all */
> > arrows(C) = m    /* the underlying set of your monoid */
> > id(m) = 0        /* the identity of your monoid */
> > (a @ m & b @ m) => comp(a, b) = a + b
> >                   /* wasn't that nice and simple? */

>

Indeed. But I needed a bit more detail*:

1. ALL(a):[a @ nodes <=> a=m]

2. ALL(f):[f @ arrows <=> f @ m]

3. id(m)=0

4.* ALL(f):[f @ arrows => source(f)=m]

5.* ALL(f):[f @ arrows => target(f)=m]

6.* ALL(f):[f @ arrows(m,m) <=> f @ arrows]

7. ALL(f):ALL(g):[f @ arrows & g @ arrows => comp(f,g)=f+g]

I reduced my proof to 236 lines. Thanks for the tip!

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.