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