Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Re: The Monoid Category in DC Proof
Posted:
Nov 10, 2012 1:17 AM


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 notnecessarilyAbelian 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



