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 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 head-to-tail) 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
|
|
|
|
