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



Re: The Monoid Category in DC Proof
Posted:
Nov 9, 2012 2:12 PM


(Corrections)
WHAT IS A CATEGORY?
Informally, a category can be thought of as a kind of directed graph  a collection of nodes connected by arrows. Each arrow has a source and target node. An ordered pair of arrows with compatible sources and targets can be composed (placed headtotail) to obtain another arrow (like the addition of vectors).
Using 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. They are reversed from the usual, less intuitive presentation.
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))]]
The 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 A 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 using the axioms of set theory such that:
ALL(a):[a @ m => i(a)=a]
Now we reconstruct the monoid in terms of nodes, arrows, sources, etc.
The only element in the set of nodes is the 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 pairs of arrows 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 a category.
Comments?
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



