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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

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: 8,219
Registered: 7/9/08
The Monoid Category in DC Proof
Posted: Nov 9, 2012 10:43 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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

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

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

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]

+ 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

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

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


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-2018. All Rights Reserved.