The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: The Monoid Category in DC Proof
Replies: 7   Last Post: Nov 11, 2012 10:37 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 6,592
Registered: 7/9/08
Re: The Monoid Category in DC Proof
Posted: Nov 9, 2012 2:12 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply



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

1. ALL(f):[f @ arrows => source(f) @ nodes]

@ = 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]

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

id(a) is the identity arrow for node a

8. ALL(f):[f @ arrows => ALL(a):[a @ nodes => [source(f)=a =>

9. ALL(f):[f @ arrows => ALL(a):[a @ nodes => [target(f)=a =>


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]

+ 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


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,

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

2. ALL(f):[f @ arrows <=> EXIST(a):[a @ m & ALL(b):[b @ m => f(b)=b

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

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.


Download my DC Proof 2.0 software at

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2017. All Rights Reserved.