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



The Monoid Category in DC Proof
Posted:
Nov 9, 2012 10:43 AM


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]]]
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)]
+ is associative
What is the monoid category?
The monoid category m is a category based on the monoid (m,+).
Before constructing the monoid category, it should be noted that on every set m, we can construct a unique identity function i such that:
ALL(a):[a @ m => i(a)=a]
Now reconstruct the monoid in terms of nodes, arrows, comp, etc.
The only element of the set of nodes is the underlying set m:
1. ALL(a):[a @ nodes <=> a=m]
The set of arrows is the set of unary functions on the set m such that:
2. ALL(f):[f @ arrows <=> EXIST(a):[a @ m & ALL(b):[b @ m => f(b)=b +a]]]
Since m is a set, we can construct the set of arrows using the axioms of set theory.
The source of all arrows is just m itself:
3. ALL(f):[f @ arrows => source(f)=m]
Likewise, for the target of all arrows:
4. ALL(f):[f @ arrows => target(f)=m]
Since there is only one node m, we can define the set of arrows with source a and target b as follows:
5. ALL(f):[f @ arrows(m,m) <=> f @ arrows]
We define the composition of these arrows is defined as follows:
6. ALL(f):ALL(g):[f @ arrows & g @ arrows => comp(f,g) @ arrows]
7. ALL(f):ALL(g):ALL(h):[f @ arrows & g @ arrows & h @ arrows => [comp(f,g)=h <=> ALL(a):[a @ m => h(a)=g(f(a))]]]
We define the id function on the only node m at follows:
8. id(m)=i
where: i is the identity function on m as defined in above.
It can be formally shown (in 549 lines in DC Proof) that this reconstruction of the monoid does indeed meet all the requirements of category.
Comments?
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



