Motivation

Category Theory is a way for talking about the relationships between the classes of objects modeled by mathematics and logic. It is a model of a collection of things with some structural similarity. It is a comparatively recent abstraction from the various abstract algebras developed in the early part of the 20th century.

The best source for detailed information is still Madc Lane's classic graduate text MacLane71.

The original use of the term category was in the idea of a 'categorical' axiom system - an axiom system which defined its objects so exactly that all objects that satisfied the axioms were isomorphic - they mapped into each other, one-to-one, preserving all the axioms and structure. This is important, because if a logic is categorical and there exists a simple (or cheaply implemented) example then that model can become the standard and all others are handled in terms of this standard. For example binary numbers have all the properties that one can expect of objects that satisfy the rules that describe a "natural number" and are cheap to emulate using electronics. The name for such ideal systems has been changed several times in this century - categorical, free, universal, initial,...

Many times category theorists have discovered that some results that they have uncovered have been discovered within a totally different area - say the theory of languages and automata. Equally often an enterprising researcher in mathematics of computer science has found that category theory allowed them to express a specific property they had observed in more general terms. The more general veiw then leads to shorter and simpler proofs of more results. This in turn often illuminates other problems.

Trivial Example

Draw three dots at the corners of a roughly equilateral triangle and call them a, b, and , c. These are your
1. YourObjects::= {a, b, c}.

   On each dot draw a little looping arrow that goes out of the dot and back to it. Label these three arrows 0. They are called identity morphisms.

2. a-0->a.
3. b-0->b.
4. c-0->c.

   You now have a very impoverished (discrete) little category with three objects and three morphisms.

   Draw an arrow from a to b and label it 2. This is your first real morphism:

5. a-2->b.

   Then add two more (quickly) to the other two sides of the triangle:

6. b-1->c,
7. a-3->c.

   Here is a complete list of all the morphisms:

8. your_morphisms::=following,
   • a-0->a.
   • b-0->b.
   • c-0->c.
   • a-2->b.
   • b-1->c.
   • a-3->c.

   You had to add both b-1->c and a-3->c at quickly because in a category each pair of adjacent arrows

9. x-->y-->z must be completed by a third arrow
10. x------>z

    Two complete the category we must give the rule for composing adjacent labels. Normal addition will do in this little category:

11. 3 = 1+2.
12. 1 = 0+1
13. etc.

Trivial Exercise

1. Draw three dots at the corners of a roughly equilateral triangle and call them 1, 2, and , 3. These are your
2. Objects::= {1,2,3}.
3. On each dot draw a little looping arrow that goes out of the dot and back to it.
   Label these three arrows 0. They are the identity morphisms for your category.
   Draw an arrow from 1 to 2 and label it 1. This is your first real morphism. You still have a category.
   Then add an arrow from 2 to 3 an label it 1. This is a second morphism.
4. Can you figure out what arrow is missing and what a good label would be?
5. You can see the answer at [ Answer to Trivial Exercise ] below.

Theory

A Category is a mixture of an algebra and a directed graph. To see how a category could be defined within graph theory see [ CATEGORY in math_22_graphs ] for example. What follows is a more traditional development.
1. CATEGORY::=
   Net{

   A category has objects and morphisms.
   1. Objects::Sets=given.

      I will abbreviate this

   2. ob::=Objects::Sets.

      A category also has morphisms that connect the objects. We think of the objects as boxes and the morphisms as arrows connecting pairs of objects.

   3. morphisms::@ARROW=given,

      By analogy with sets and mappings, one end of the arrow we call the Domain and the other the Codomain, but we notice that the is no necessity for the arrows to actually be mappings. Others use words like source and target. The arrows are labeled.

   4. labels::Sets = given.
   5. ARROW::=Net {Dom, Cod : Objects, label : labels},

      We can encode an arrow connection object o1 to o2 with label m by the string o1-m->o2. We give a context dependent meaning: it can be the Arrow connecting o1 to o2 with label m:

   6. For m:labels,o1,o2:ob, o1-m->o2::ARROW=the ARROW(Dom=>o1, label=>m, Cod=>o2).

      The same notation will be overloaded to express the proposition that such an arrow exists with a particular label, source, and target, in the category under consideration:

   7. For m:labels,o1,o2:ob, o1-m->o2::@=(Dom=>o1, label=>m, Cod=>o2) in morphisms.

      Note. Some use "n:X->Y" for X-n->Y. This would be ambiguous in MATHS.

      So we have a set of relations:

   8. For m:labels, (-m->) ::=rel[o1,o2]( o1-m->02 ).

      So we write can a path of alternating boxes and arrows (objects and morphisms) out like this

   9. X-a->Y-b->Z-c->W

      and mean

   10. X-a->Y and Y-b->Z and Z-c->W.

       because relations are parallel operators in STANDARD MATHS.

       Whenever a pair of arrows share a common point: a-mab->b-mbc->c then we are given a way of composing the labels (traditional written o) and an arrow connecting the outer pair a to b . In this case: a-(mbc o mab)->c.

       I often feel that composition is backwards and so define

   11. m1; m2::= m2 o m1,

       so that,

   12. For all A-f->B-g->C, A-f;g->C.

       Notice the abuse of notation:

   13. for all X-a->Y(P)::= For all X, Y: Objects, a: mo(X, Y) (P).
   14. for some X-a->Y(P)::= For some X, Y: Objects, a: mo(X, Y) (P).

       and so on. In other words the category defines the rules of composition of the morphisms.

   15. compatible::@(morphisms><morphisms)={(f, g):morphisms><morphisms || Cod(f)=Dom(g)}

   16. composition::compatible->morphisms=given, `the composition of (1st) and (2nd)`,
   17. o::infix=composition.

       Each object has a special morphism that is called an identity. If X is an object then X's identity is id(X) and it connects the object to itself:

   18. id::Objects->morphisms=given, the identity morphism.

       
       

   19. |- (cat1): for all X:Objects, X-id(X)->X.

       We often omit the'(X)' when this is clear from the context:
       

   20. |- (cat2): X-id->X iff X-id(X)->X.

       The identity has the important property of not changing morphisms when composed with them:

   21. m o id = id o m= m.

       This will be defined formally below.

       We can define an abreviation 'mo(X,Y)` for the set of morphisms connecting X with Y:

   22. morphisms::(Objects><Objects)->@morphisms=map [X, Y]{f || Dom(f)=X and Cod(f)=Y}.
   23. mo::=morphisms.
       
   24. (def)|- (mo0): for X,Y:objects, mo(X,Y)={ X-m->Y:ARROW || X-m->Y}.

       
       

   25. (above)|- (mo1): For all U,V,X,Y:objects, if mo(X, Y) & mo(U, V) then X=U and Y=V.
       
   26. |- (mo2): morphisms>=={mo(X,Y) || X,Y:ob}.

   27. For f:mo(X,Y),g:mo(Y,Z), h:mo(Z,W), f o g o h::= (f o g) o h.

       
       

   28. |- (comp1): For all X,Y,Z:ob, f:mo(X,Y), g:mo(Y,Z), f o g in mo(X,Z).

       
       

   29. |- (comp2): For f:mo(X,Y),g:mo(Y,Z), h:mo(Z,W), f o (g o h) = (f o g) o h.

       
       

   30. |- (comp_is_serial): SERIAL(morphisms, "o", (o)),

       All objects have identities:
       

   31. |- (id0): For all X, Id(X) in mo(X,X). Further an identity morphism does nothing: when composed with another morphism, it leaves that morphism unchanged.

       
       

   32. |- (id1): For all X,Y:ob, f:mo(Y,X), id(X) o f = f.
       
   33. |- (id2): For all X,Y:ob, g:mo(X,Y), g o id(X) = g.

       We can show that there can be no more than one Identity morphism per object. First define the generic forma of an identity.

   34. IDENTITY::=
       Net{

       1. X::ob,
       2. i::mo(X,X),
       3. for all Y:ob, f:mo(Y,X),g:mo(X,Y)( g o i=g and i o f= f).
       4. }.

          Hence the uniqueness of Id(X) for all X.
          

       5. (id0, def)|- (id3): For all X, 0..1 i(IDENTITY(X,i)).
          
       6. (id1, id2)|- (id4): For all X (IDENTITY(i=>Id(X))).
          
       7. (id3, id4)|- (id5): For X, Id(X)=the i(IDENTITY).

          Hence we can prove that each object has a monoid:
          

       8. (above)|- (mon_obj): for all x:ob ( MONOID( mo(x,x), o, id(x) ) ).

       
       }=::CATEGORY.

   35. Category::=CATEGORY.

       Examples

       Matrices

       Matrices are rectangular arrays of numbers that represent linear mappings. They have a form of multiplication. But not all matrices can be be multiplied. Each matrix has a number of rows and a number of collumns. Two matrices can be multiplied, if, and only if, the neumber of columns in the first equals the number of rows in the second.

       We can model this by saying that we have a category whose objects are the natural numbers: 1,2,3,.... and whose morphism are the matrices. A matrix with R rows and C columns is a morphism from object R to object C.

       Sets and relations between them

       
       
       1. (above)|-CATEGORY(objects=>Sets, morphisms=>Relations, Dom=>dom, Cod=>cod, o=>o, id=>Id)
          
       2. (above)|-For all arrow:{->, >->,-->,>--,>==,==>,>=>,<>->,---,...}, mo:=map[X,Y]{ X-f->Y || f:X arrow Y}, CATEGORY(Sets, mo, Dom=>dom, Cod=>cod, o=>o, id=>Id).

          Algebraic Systems with homomorphisms

          
          
       3. (above)|-For all systems:{poset, unary, semigroup, monoid, group, ..., continuous, topology, ...}, arrows:{->, >->,-->,>--,>==,==>,>=>,<>->,---,...}, mo:=map[X,Y]{ X-f->Y || f:(system)X arrow Y}, CATEGORY(Sets, mo, Dom=>dom, Cod=>cod, o=>o id=>Id).

          Directed Graphs

          
          
       4. (above)|-For all G:DIGRAPH, CATEGORY(ob=>nodes, mo=>map[X,Y](if ( X<>Y, {X-p->Y || p in X..Y}, { X-Id->X }),...}

       . . . . . . . . . ( end of section Examples) <<Contents | End>>

       Subcategories

       A subcategory has some of the objects and morphisms of another category and is itself a category:
   36. SUBCATEGORY::=
       Net{

       
       
       1. |- (sub0): CATEGORY(C),
       2. D::@objects(C),
          
       3. |- (sub1): for X,Y:D, D(X,Y)==>C(X,Y),
          
       4. |- (sub2): for X:D, C.Id(X)=D.Id(X).
          
       5. (sub0, sub1, sub2)|- (sub3): CATEGORY(D).

       
       }=::SUBCATEGORY.

   37. FULL_SUBCATEGORY::=Net{SUBCATEGORY,for X,Y:D, D(X,Y)=C(X,Y)}.

       Diagrams

       1. Commutative_Diagrams::=
          Net{

          
          
          1. |- (CD0): CATEGORY(C),
          2. D::=DIGRAPH(Nodes=>@C.ob, Arcs=>@C.morphisms), Each path in D determines a sequence of morphisms and so their composition:
             
          3. |- (CD1): For p:path, o(p) in mo(1st(p), last(p)),

             The diagram commutes if for all different paths with the same end points define the same morphisms:

          4. commutes::@=for all X,Y:C.ob, p1,p2:X..Y, o(p1)=o(p2).

             Examples of Commutative_Diagrams

             Example Diagram of Composition

             Traditionally composition is defined by showing a figure

             Figure 0

             The Triangle (c=b o a)

                      a

                   X---->Y

                    \    |

                     \c  |b

                      \  |

                       \ |

                        \V

                         Z

             where the diagonal line should be a dotted line. This means that that the dotted line is uniquely determined by the others lines.

             In ASCII use a horizontal layout with "stretched arrows":

                 Dom---map--->Cod

             And with equal objects aligned vertically [ Figure 1 ] below.

             Figure 1

                 X-a->Y-b->Z

                 X----c--->Z

              Define for all X, Y, Z, a, b, a o b::=the c(Figure 1).

             If we add successive quantifiers and predicates as we go

              all   X-a->Y-b->Z

              one   X----c--->Z

             we can use the diagrams to assert properties in a fairly obvious way.

             Example of Defining Identity via ASCII diagrams

              All nodes have an identity morphism:

                 For all X, some i(IDENTITY2), where

              IDENTITY2:=Net{

                 for all Y,f,

                      X--i->X-f-->Y

                      X-------f-->Y

                 for all Y,g,

                      X<-i--X<-g--Y

                      X<-------g--Y

              }.

             Example: Commutivity

             The "Square Diagram" for b o a=d o c,
             1. SQUARE::=
                Net{

                 all   W-a->X--b-->Z

                 all   W--c-->Y-d->Z

                
                }=::SQUARE.

                        a

                     W----->X

                     |      |

                     |c     |b

                     |      |

                     V  d   V

                     Y----->Z

             . . . . . . . . . ( end of section Examples of Commutative_Diagrams) <<Contents | End>>

          
          }=::Commutative_Diagrams.

       . . . . . . . . . ( end of section Diagrams) <<Contents | End>>

       Constructing New categories.

       Given a category C then there exit large numbers of other categories that can be constructed, tinker-toy fashion from it.

       For example there is a category of all the morphisms going to a particular object. If C is a category and X:C.ob then define comma(C,X).ob ::= |{mo(A,X) || A:C.ob}, comma(C,X).mo ::= [A1-f1->X, X<-f2-A2]{g:C.mo(A1,A2) || f2 o g=f1}

       The more popular notation being

   38. C over X::= comma(C,X).

       Any commutative diagram can be taken as a template or pattern for a set of objects in a new category and then morphisms between diagrams defined as lists of morphisms between corresponding nodes in the diagrams.

       In many cases a simple way to prove a property of some set of objects or construction is to construct a category in which the particular case is a privileged object - initial or final, typically.

       Isomorphisms

       A morphism X-g->Y is an isomorphism if it has an inverse Y-/g->X:
   39. inverse(g)::={ f: mo(Y,X). f o g = id(Y) and g o f = id(X) }.
   40. ISOMORPHISM::=
       Net{

       
       
       1. |- (I0): CATEGORY(C).
       2. isomorphism::mo(X,Y).
       3. iso::=isomorphism.
          
       4. |- (I1): For some g(g o iso =id(Y) and iso o g =id(X)).

       5. Figure_2::=following,
          Net

           X-iso->Y--g-->X

           X-----id----->X

          and

           Y--g-->X-iso->Y

           Y-----id----->Y

          
          (End of Net Figure_2)
          
          

          
          

       6. (above)|- (unique): for one g(Figure_2)

          Proof of unique

          
          Let
          
          
          1. |- (f11): g1,g2:C.morphisms,
             
          2. |- (f12): g1 o iso=id and iso o g1 = id,
             
          3. |- (f13): g2 o iso=id and iso o g2 = id.
             
          4. (f13)|- (f14): g1 o iso o g2 = g1 o (iso o g2)=g1 o id = g1.
             
          5. (f12)|- (f15): g1 o iso o g2 =(g1 o iso) o g2=id o g2 = g2.
             
          6. (f14, f15)|- (f16): g1 = g2
          
          (Close Let )
          
       7. For iso, /iso::=iso^-1::=the g(Figure_2).

       
       }=::ISOMORPHISM.

   41. isomorphisms(C)::=$ ISOMORPHISM.isomorphism

       for X,Y:C, X isomorphic Y::@=isomorphisms(C)& mo(X,Y), there are isomorphisms connecting X and Y.

   42. GROUPOID::= CATEGORY and {for all X-m->Y( some inverse(m)},
   43. groupoid::= $ GROUPOID.

       Duality

       By reversing all the arrows in a category we get the dual category. By reversing all the arrows in a diagram we get the dual diagram. This means that for just about any concept defined in categorical terms there is a dual concept generated by reversing arrows. Typically, if we have defined an idea I then it's dual is named co-I. A classic example is product and coproduct.

   44. DUALITY::=
       Net{

       |-(D0): C, C'::CATEGORY,
       
       1. |- (D1): C'.ob=C.ob,
          
       2. |- (D2): C'.id=C.id.
          
       3. |- (D3): for all X,Y:C'.ob (C'.mo(X,Y)=C.mo(Y,X)),
          
       4. |- (D4): for all X,Y,Z:C.ob, f,g: C.mo, X-f->Y-g->Z (f(C'.o)g=f(C.o)g ).

       
       }=::DUALITY.

   45. For C:CATEGORY, dual(C)::=DUAL(C)

       Some write C^op for dual(C).

       Free Objects

       Free objects have an unique position in a category. The term free is a holdover from algebra. We can distinguish two types of free objects: those that are attract one arrow from all other objects in the rest of the category, and those that start an arrow to every object in a category.

       
       (inversally_repeling): Some objects are called "initial objects". They were also called "universally repelling objects" because all their arrows appeared to be pushing the other objects away. Carl Linderholm has noted that mathematicians find universally repelling objects universally attractive [Carl E. Linderholm. Mathematics Made Difficult. Wolfe, London, 1971] (thanks to Scott Wakefield of MicroMagic for this reference).

   46. INITIAL_OBJECT::=
       Net{

       1. Cat::CATEGORY,
       2. an_initial_object::Cat.ob,
          (IC0): For all X, one Cat.mo(an_initial_object,X).
       3. I::=an_initial_object.
       4. For all X, (I-!->X) ::= the(Cat.mo(I, X)).

       
       }=::INITIAL_OBJECT.

   47. TERMINAL_OBJECT::=
       Net{

       1. Cat::CATEGORY,
       2. a_terminal_object::C.ob,
          (TC0): For all X:C.ob, one Cat.mo(X, A).
       3. A::=a_terminal_object.
       4. For all X, (X-?->A) ::= the(mo(X, A)). In Manes and Arbib an upside down exclamation mark is used for the unique arrow that points at a terminal object from other objects.

       
       }=::TERMINAL_OBJECT.

   48. For C:CATEGORY, initial_objects(C)::={I:C.ob || INITIAL(C, A)}.
   49. For C:CATEGORY, terminal_objects(C)::={A:C.ob || TERMINAL(C, A)}.

       
       

   50. (above)|- (IC1): For C:CATEGORY, A, B:initial_objects(C), (A-!->B) in isomorphisms(C).
       
   51. (above)|- (IC2): For C:CATEGORY, A, B:initial_objects(C), A isomorphic(C) B.

       Because all initial objects are isomorphic(IC1 above) we tend to speak about the initial object. Similarly with the terminal object.

       
       (free): Another term used for an initial object is "the free object". The reason for this is that in the category of all algebras of a given type plus the usual homomorphisms between them the initial objects turn out to be "free of any constraint" because homomorphisms express constraints.

       Example of a Free Algebra

       Consider all monoids with two generators {a,b}, have MONOID(#{a, b},!, ()) as an initial object in the category with monoid homomorphisms. So, any monoid generated by {a, b} is a homomorphic image of (#{a, b},!,() ) - by a unique homomorphism. This homomorphism is determined by a unique kernel set in @#{a,b} called the set of relators. Often these are written as equations like a*b=1 or a*a=1. Since the kernel of the identity map for #{a,b} is {()} we say that #{a,b} is free of all constraints.

       Initial Objects are a good model for data types.

       This and many similar examples of initial objects in algebras that encode any other member of the class leads computer scientists to the idea that ALL data types are best defined as initial objects (initial algebras). A MATHS type can be thought of as an initial object in the category of all sets of things that have the particular components, maps and properties defined - the Σ-algebras.

       
       

   52. (above)|- (TC1): For C:CATEGORY, A, B: terminal_objects(C),(A-?->B) in isomorphisms(C).
       
   53. (above)|- (TC2): For C:CATEGORY, A, B: terminal_objects(C), A isomorphic B.

       Example initial and terminal objects in the category of sets

       The type of all Subsets (@T) of a given type(T) of element equipped with all mappings between subsets as morphisms is a category. It is easy to show
   54. {}=initial_object(Sets),
   55. @T1 ==>terminal_objects(Sets).

       Zero Morphisms

   56. For C, zero_morphisms(C)::C.ob><C.ob->@ morphisms,
   57. 0::=zero_morphisms.
   58. For all X,Y,W,Z:mo(C), f,g:morphisms, z1:0(W,Z), z2:0(X,Y) (Figure 2)
   59. Figure_3::=following,
       Net

           W-z1->Z--g-->Y

           W--f->X--z2->Y

       
       (End of Net Figure_3)
       
       

       
       

   60. |- (ZM): for 0..1 zero_morphisms.

       Example of Relations between Elements in a Set

       CATEGORY(Sets, Relations).
   61. 0(X,Y)=({}:@(Sets,Sets))=({}-!->X) o (Y-?->{}).

       for C:category, zero_objects(C) ::=initial_objects(C) & terminal_objects(C).

       
       

   62. |- (ZM1): for C, some zero_morphisms(C) iff some zero_objects(C).

   63. For C, if some zero_morphisms(C) then total_morphisms(C) ::={f:mo(X,Y)|for all t:mo(T,X)(if t<>0 then f o t<>0}

       
       

   64. |- (ZM2): f,g:total_morphisms then g o f in total
       
   65. |- (ZM3): if g o f in total_morphisms then f in total_morphisms.

       Classifying morphisms

       Inspired by mappings between sets, you can separate morphisms into monomorphisms, epimorphisms, isomorphisms, and the rest. In algebra and logic these are defined by using elements. In category theory we use morphisms instead. We also have another terminology: monic and epic morphisms.

   66. MONIC::=following,
       Net
       
       
       1. |-CATEGORY X, Y :: Objects,
       2. m::mo(X,Y).
          
       3. |-for all A-f->X, A-g->X ( if m o f = m o g then f=g )}.

           	A-f->X-m->Y

           	A-g->X-m->Y

       
       (End of Net)
       
       
   67. monic::@morphisms={m. for some X,Y (MONIC)}
   68. EPIC::=following,
       Net
       
       
       1. |-CATEGORY X, Y :: Objects,
       2. m::mo(X,Y).
          
       3. |-for all Y-f->A, Y-g->A ( if f o e = g o e then f=g )}.

       
       (End of Net)
       
       
   69. epic::@morphisms={e. for some X,Y (EPIC)}

       Products in categories

       These are abstracted from the idea of a Cartesian product in sets. They turn out to be definable for most algebras and logistic systems.

       He is a simple special case. A product of two objects (if it exists) is an object that has two special projection morphisms that extract the original objects from the product. If XY is a product of X and Y then there are special morphisms XY-x->X and XY-y->Y which extract the maximum amount of Xness and Yness out of XY. So, for any other object Z with morphisms Z-zy->Y and Z-zx->Y, we require a morphism Z-zxy->XY so that x o xyz = zx and y o xyz = zy.

        X<-x--XY--y->Y

        |     ^      |

        =    zxy     =

        |     |      |

        X<-zx-Z -zy->Y

       In general we can define a product of any number of objects. First we define the indexed collection of morphisms into(out of) a indexed collection of objects,

   70. For C:CATEGORY, I:Sets, α:I->C.ob, Y:C.ob,
   71. C(Y,α)::={f:I->C.morphisms || for all i:I(f(i) in C(Y,α(i)) )},

        f in C(Y,\alpha) iff

        for all i

                      Y-f(i)->\alpha(i)

   72. For C:CATEGORY, I:Sets, α:I->C.ob, Y:C.ob,
   73. C(α,Y)::={f:I->C.morphisms || for all i:I(f(i) in C(α(i),Y) )}.

        f in C(\alpha,Y) iff

        for all i

                      \alpha(i)-f(i)->Y

       
       

   74. |- (pair): for Y,A,B, C(Y,(A,B))={(a,b):C.morphism^2 || a:C(Y,A), b:C(Y,B) }.
       
   75. |- (string): for X:#C, C(Y,X)={a:#C.morphisms || for all i:1..|X|(a(i) in C(Y,X(i))}.

   76. PRODUCT::=
       Net
       1. category::CATEGORY=given,
       2. index::Sets,
       3. C::= category,
       4. I::=index,
       5. components::I->C.ob,
       6. α::=components.
       7. product::C.ob,
       8. P::=product.
       9. projections::C(P,α).
       10. th::=projections.
       11. pr::=projections.

            For all i

                                 P-pr(i)->\alpha(i)

           
           

       12. |- (Pr0): For all Y:C.ob, f:C.mo(Y,α), one p:C.mo(Y,P), all i(i.th o p = f(i)).

           For all Y, f, if for all i

                         Y-------f(i)->\alpha(i)

           then for one p

                         Y-------f(i)->\alpha(i)

                         Y-p->P

           and for all i

                         Y-------f(i)->\alpha(i)

                         Y-p->P-pr(i)->\alpha(i)

       
       (End of Net PRODUCT)
       
       

       Products can also be given a categorial construction as a terminal object in a different category:

   77. D::CATEGORY( objects=>{(Y,f) || Y:C.ob, f:C.mo(Y,α)}, morphisms=>{(Y1,f1)-h->(Y2,f2)|| for some h:C.mo(Y1,Y2), all i:I(f1(i)=f2(i) o h)}),

       
       

   78. (above)|- (Pr2): (P, th) in terminal_objects(D)

       
       

   79. (above)|- (Pr3): For all I, α, if (I,α,P,th), (I,α,P',th') in PRODUCT then P isomorphic P'.

   80. ><::{ (I->C.ob)->C.ob | I:Sets},

       
       (Pr4): For all I,α,some th (PRODUCT(P=> ><α)).

   81. For all I,α, Y:C.ob, f:C.mo(Y,α), ><f::=the p:C.mo(Y,><α)(for all i(i.th o p = f(i))). .The Product Diagram
   82. Figure_4::=following,
       Net

        Y-(><f)->(><\alpha)-i.th->\alpha(i)

        Y---------f(i)----------->\alpha(i)

       
       (End of Net Figure_4)
       
       

       In typeset/written documentation a prefixed "><" is shown as a large capital "Π".

       
       

   83. (above)|- (Pr5): if ({},X,P,th) in PRODUCT then P in terminal_objects.

       See Cartesian products in [ logic_5_Maps.html ] , [ math_13_Data_Bases.html ] , and [ types.html ] for examples.

       This theory motivated and supports the definition of a generalization of the n-tpl or record structure in terms of projection maps only. This in turn leads to the idea that most pieces of documentation describe a structure (up to isomorphism) and we can adopt the free/universal/initial object as the standard set of objects that satisfy that documentation.

   84. For example let UNIT_CIRCLE::=Net{x,y:Real, x^2+y^2=1}. UNIT_CIRCLE is a set of documentation that describes a large number of possible logics, but the following U is universal (upto isomorphisms):
   85. U::={(a,b):Real^2 || a^2+b^2=1} with
   86. x::U->Real=1st.
   87. y::U->Real=2nd. and so we write
   88. U=$ UNIT_CIRCLE.

       Co-Products

       These are the dual of products. They are a natural generalization of the "Discriminated Union" of Types found in some programming languages. Category theory shows that in most known algebras and logistic systems, there is a way to construct an equivalent.

       The definitions are identical except that we write "\/" in place of "><" and reverse all the arrows. An upside down capital greek Π (\Ip \iP ??)is a common typeset symbol.

       Thus for I:Sets, X:I->Sets, \/X::=|{X(i)><{i} || i:I}, so that for each i there is a unique map inj(i) or map[a](a,i) that injects X(i) into \/X.

       In general, co-products are described by:

   89. For C:Category, I:Sets, X:I->C.ob, define \/X upto isomorphism by
   90. For all Y, f:C(X,Y), (

           Y<-(\/f)-(\/X)<-i.inj-X(i)

           Y<--------f(i)--------X(i)

       )

       Pushouts

       A pushout is a kind of loose co-product: a pair of objects have a push out which has a an overlap allowed on a third object. But: this is defined in terms of a combination of two morphisms: For

        all	c<------g--a-------f------->b

   91. r is_a_pushout(f,g)::=following

        some	c--v--->r<------------u-----b

        all	c----k-------->s<---h-------b

        one	        r--t-->s

       [click here if you can fill this hole]

       Pullbacks

       These are the dual of pushouts. [click here if you can fill this hole]

       Products of Categories

       Given a couple of Categories B and C, we can construct, in a natural way, a new category that is a product of B and C:
   92. PRODUCT::=following
       Net
       1. B:: $ CATEGORY.
       2. C:: $ CATEGORY.
       3. B><C:: $ CATEGORY = (op=> B.ob><C.ob, mo=> {(f><g). f:B.mo, g:C.mo}, o=>((f',g'),(f,g)+> (f' o f, g' o g) ).

       
       (End of Net)
       
       

       Diagonal Product

   93. Δ(D)::$ CATEGORY = D><D.

       Adjoints

       For many categories there is an adjoint category that can be constructed from it. [click here if you can fill this hole]

       Functors

       A category is an abstract mathematical model of how mathematical systems are related together. For example, Sets and maps, Monoids and homomorphisms,... Functors arise naturally in the semantics of data types because here we our concerned with operations on both objects and also on the operations on those objects.

       A functor is at another level of abstraction - here we take a set of categories and treat them as objects, and look for a natural, mapping between them that preserves their structure - preserves objects and preserves morphisms between objects.

       A simple example is DUAL which reverses all the arrows in a category. DUAL defines a functor between a category and its dual.

   94. FUNCTORIALITY::=
       Net{

       
       
       1. |- (F0): CATEGORY(C).
          
       2. |- (F1): CATEGORY (D).
       3. \psi::C.ob->D.ob & C.morphisms->C.morphisms.

          
          

       4. |- (F2): For all c1,c2:C.ob,f:C.mo(c1,c2), f.\psi in D.mo(c1.\psi, c2.\psi).

          
          

       5. |- (F3): For all c:C.ob, \psi(id(c))=id(\psi(c)).

          
          

       6. |- (F4): For all c1,c2,c3:C.ob, f21:C.mo(c1,c2), f32:C.mo(c2,c3),
       7. \psi(f21) in D.mo(\psi(c1),\psi(c2))
       8. and \psi(f32) in D.mo(\psi(c2),\psi(c3))
       9. and \psi (f32 (C.o) f21) in D.mo(\psi(c1),\psi(c3))
       10. and \psi (f32 (C.o) f21) = \psi(f32) (D.o) \psi(f21).

           
           

       11. |- (F5): \psi(C.isomorphisms) ==> D.isomorphisms

       
       }=::FUNCTORIALITY.

   95. For C,D:categories, (functor)C->D ::= {\psi || FUNCTORIAL}.
   96. For :categories, endofunctors(C)::= (functor)C->C.

       Functors are also easily seen to be generalisations of the monotonic (order preserving) mappings defined in partially ordered sets as part of the semantics of recursive calculations.

       Often its enough to show a diagram:

        C:      c1-f21->c2

        \psi    |   |   |

        D:      d1-g21->d2

       Examples:
   97. For C,D:Categories,
       (Constant): d:D.ob, \psi= (C.ob->map[c]d | C.morphisms->map[m](d-id->d) ),

        C:      c1-f21->c2

        \psi   |  |   |

        D:       d--id->d

       
       (Identity): C=D, \psi= map[x:C.ob|C.morphisms]x

        C:      c1-f21->c2

        \psi  |   |   |

        D:      c1-f21->c2

       
       (Dual): C.ob=D.ob, C.mo(c1,c2)=D.mo(c2,c1)

        C:      c1--f21->c2

        \psi  |    |   |

        D:      c1<-f12--c2

   98. For C,D:Categories and PRODUCT(><),
   99. for n:Nat, d,e:array(1..n) of D.ob, f:array(1..n)of D.morphism,
   100. for i:1..n( d[i]-f[i]->e[i] and (i.th o ><f) = (f[i] o i.th) ),
   101. for \psi:array(1..n) of (functor)C->D,

   102. ><\psi:(functor)C>-D

         C:      c1----------------------f----------------->c2

         \psi   |                      |                   |

         D:      ><[i]\psi[i](c1) - ><[i]\psi[i](f) -----> ><[i]\psi[i](c2)

        Similarly for the dual co-product structure with \/ in place of ><.

        Functor Composition

   103. For C,D,E:Categories, \psi:(functor)C->D, φ:(functor)D>-E,
   104. φ o \psi in (functor)C->E.
   105. (φ o \psi)(c) = φ(\psi(c))
   106. (φ o \psi)(m) = φ(\psi(m))

        ?? replace '->' by other arrows...in FUNCTORIALITY? [click here if you can fill this hole]

        Functor Products

        We can also consruct products of functors... which map between the products of the domain and codomain of the functors.

        Natural Transformations

        These are the next level of insanity. They are transformations that act between functors. Some would call them morphism between functors.

        An Alternate Basis

        Peter Freyd & Andre Scedrov [FreydScedrov90] present a simpler but more absract formulation of the idea of a category by focusing entirely on the arrows/morphisms:
        1. FS_CATEGORY::=following
           Net
           1. Morphism::Sets.
           2. For x:Morphism, \box x::Morphism=the source of x.
           3. For x:Morphism, (x \box) ::Morphism=the target of x.
           4. For x,y:Morphism, defined(x, y)::@= ((x\box)=(\box y)).
           5. For x,y:Morphism, if defined(x, y), (x y) ::Morphism=`the composition of x and y`.
           6. Ids::=Identity_morphism.
           7. Identity_morphism::@Morphism={ e. for some x( e = \box x ).

              
              

           8. |- (SF1a): ((\box x)\box)=(\box x).
              
           9. |- (SF1b): (\box(x \box))=(x \box).
              
           10. |- (SF2a): (\box x)x = x.
               
           11. |- (SF2b): x(x \box) = x.
               
           12. |- (SF3a): \box(x y) = \box(x(\box y)).
               
           13. |- (SF3b): (x y)\box = ((x \box) y)\box.
               
           14. |- (SF4a): For x,y,z:Morphisms, defined(y,z) and defined(x,(y z)) iff defined(x, y) and defined((x y), z).
               
           15. |- (SF4b): For x,y,z:Morphisms, x(y z) = (x y) z.
               
           16. (above)|- (SF5): if defined(x,y) then \box(x y)= \box x.
               
           17. (above)|- (SF6): \box(\box x) = \box x.
               
           18. (above)|-Ids = {e. for some x(e = x \box)} = { e. e = \box e} = {e. e=(e\box)}.
               
           19. (above)|-Ids = {e. for all x(if defined(e,x) then (e x)=x}.
               
           20. (above)|-Ids = {e. for all x(if defined(x,e) then (x e)=x}.

           
           (End of Net)
           
           

           Proof of SF6

           
           Let
           1. \box(\box x) =
              
           2. (SF1a)|-
           3. = \box((\box x)\box)
           4. = (\box x)\box
           5. = \box x.
           
           (Close Let )
           

        . . . . . . . . . ( end of section An Alternate Basis) <<Contents | End>>

        Allegories

        "Basking like an allegory on the bank of the Nile" Allegories are an abstract model of relationships.
        1. ALLEGORY::=following
           Net
           
           
           1. |- (Al0): CATEGORY.
           2. For all R:Arrow, /R::Arrow = the converse of R.
           3. For all R,S:Arrow, if dom(R)=dom(S) and cod(R)=cod(S), R&S::Arrow=`the intersection of R and S`.
              
           4. |- (Al1): dom(/R)=cod(R) and cod(/R)=dom(R).
              
           5. |- (Al2): /(/R) = R.
              
           6. |- (Al3): if defined(R&S) then dom(R&S)=dom(R).
              
           7. |- (Al4): ABELIAN_SEMIGROUP(Arrow, (&)).
              
           8. |- (Al5): /(R;S) = (/S);(/R) and /(R&S)=(/R)&(/S).
           9. sub::@(Arrow, Arrow).
           10. For all R,S, R sub S::= (R=R&S).
               
           11. |- (Al6): R;(S&T) sub (R;S)&(R;T).
               
           12. |- (Al7): (R;S)&T sub (R & (R;/S));S. --(law of modularity)

           13. 1::Arrows.
           14. for all R( 1;R=R;1=R).
               
           15. ()|- (Al8): /1 = 1.
               
           16. ()|- (Al9): R sub R;/R;R.

           17. REFLEXIVE::={R. dom(R)=cod(R) and 1 sub R}.
           18. SYMMETRIC::={R. dom(R)=cod(R) and /R sub R}.
           19. TRANSITIVE::={R. dom(R)=cod(R) and R;R sub R}. [ ..] .

               Similarly we can define entire and simple relations and maps as relations that are entire and simple:

           20. ENTIRE::={R. 1 sub R;/R}.
           21. SIMPLE::={R. /R;R sub 1}.
           22. MAP::= SIMPLE & MAP.

           23. For f,g:MAP, (f, g)TABULATES R::@ = ( (/f);g = R and (f;/f)&(g;/g)=1).
           24. Tabular::@Arrow={R. for some f,g:MAP((f,g)TABULATES R}.

           25. TABULAR::@= (Tabular=Arrow).

               Proof of Al8

           26. /1 = /(/1) = /(1;/1)=/ /1;/1=1;/1=1.

               Proof of Al9

           27. R sub (1;R)& R sub (1 & (R;/R);R sub R;/R;R

           
           (End of Net)
           
           

        . . . . . . . . . ( end of section Allegories) <<Contents | End>>

        Partially Additive Categories

   107. Partially_Additive_Categories::=
        Net{

        [Manes&Arbib86]
        
        1. |- (PAC0): CATEGORY(C).
           
        2. |- (PAC1): For all X,Y:ob, PARTIALLY_ADDITIVE(X=>mo(X,Y), (+)).
           
        3. (above)|- (PAC2): For all X,Y, some zero_morphisms(X,Y).
        4. For all X, Guards(X)::={p:mo(X,X) || for some p':mo(X,X)( p+p'=id(X) and p;p'=p';p=0(X,X) )
           }.

        
        

   108. (above)|- (PAC3): FLOSET(Guards(X),+).
        
   109. (above)|- (PAC4): BOOLEAN_ALGEBRA(Guards(X))

   
   }=::Partially_Additive_Categories.

   Fixed Points of Functors

   A fixed point of a functor is not exactly an object in an category. The fixed points are fixed only upto isomorphism in this theory - an object is fixed if the functor generates a specific isomorphic object. Let functor \psi:C->C so that \psi is an endofunctor, then a fixed point of \psi is a PAIR (A,i) with i:isomorphisms(C), A:C.ob and with \psi(A)-i->A. In other words \psi's effect on A is cancelled out by an i - an i for an psi, perhaps.

   1. For \psi:(functor)C->C, fixedpoint(\psi)::= {(A,i):C.ob><isomorphism || \psi(A)-i->A }.

      \psi-algebras.

      Compare Σ.algebra in [ math_43_Algebras.html ]

   2. For C, \psi:endofunctors(C), \psi.algebras::={(A,δ) || \psi(A)-δ->A}.
   3. For C, \psi:endofunctors(C), \psi.coalgebras::={(A,Δ) || A-δ->\psi(A)}.

      Morphisms of algebras.

   4. For (\psi.algebra)(a,δ)->(B, γ) ::=
   5. {f:C.ob(A,B) ||

          \psi(A)--\psi(f)-->\psi(B)----\gamma----->B

          \psi(A)-----\delta-------->A--f---------->B

      Notice that

   6. \psi.Alg::=(ob=>(\psi.algebras), morphisms=>(\psi.algebra)) in Categories.

      Dually - \psi.coAlg in Categories.

      Fixed points of functors are universal algebras!

      
      

   7. |-For (A,δ):initial_objects(\psi.Alg), (A,δ) in fixedpoint(\psi)
      
   8. |-For (A,Δ):terminal_objects(\psi.coAlg), (A,δ) in fixedpoint(\psi)

      Example: Approximations without Domains or Metrics

      
      
   9. |-poset(P,<=).
   10. CATEGORY(objects=> P, morphism=>(<=))
   11. functors - monotonic maps
   12. fixed points: {x || \psi(x)=x }
   13. \psi_algebras: {x || \psi(x)<=x},
   14. the least{x || \psi(x)<=x}=the least fixedpoints.
   15. \psi_coalgebras:{x || x<=\psi(x)}

       Notice that

   16. increasing(\psi)::= {h || h<=\psi(h)}.
       
   17. (Tarski55)|- (Tarski_Knaster): For H:= increasing(\psi), if some lub H(\psi) then the lub H(\psi) = the greatest fixedpoint(psi).

   18. least_fixed_point(\psi)::= the initial object (\psi.Alg)
   19. greatest_fixed_point(\psi)::= the terminal object (\psi.coAlg)

       This defines what Manes and Arbib mean by the "best" approximation WITHOUT having to define a precise ordering or distance on the objects before hand [Manes & Arbib 86 ]. The structure comes out of the structures being investigated in a natural way. Compare with Domain Theory and Metric Spaces.

       This allows them to prove that the definition

   20. C::=B|A!C has two solutions: (1)C=#A B, (2)C=#A B | {map[n:Nat0](A^n)}.

       G. Plotkin, M.D. Smyth and M Wand in the 1970's worked on using the fixed points of functors to define data structures [ LehmanSmith81 ] and recent text [ Gunter 92 ] covers the theory in detail.

   . . . . . . . . . ( end of section Fixed Points of Functors) <<Contents | End>>

   Limits and CoLimits

   [click here if you can fill this hole]

   Topos

   A special kind of category that has many of the properties of sets.

2. topos::= See http://math.ucr.edu/home/baez/topos.html

   [click here if you can fill this hole]

   Bibliography

   
   (MacLane71): Saunders Mac Lane, Categories for the Working Mathematician, Springer-Verlag NY NY 1971.

   
   (Gunter 92): Gunter 92, Carl A Gunter, Semantics of Programming Languages:Structures and Techniques, The MIT press Cambridge MA 1992

   
   (Lehman & Smith 81): Lehman & Smith 81, D J Lehmann & M B Smyth, "Algebraic specification of data types", Math Systems Theory V14, 1981, pp97-139

   
   (Manes & Arbib 86): Manes & Arbib 86, Manes & M Arbib,Algebraic Approaches to Program Semantics, Springer Verlag Monograph 1986

   
   (Tarski 55): Tarski 55, A Tarski, "A Lattice Theoretical Fixed point Theorem and its Applications," Pacific Journal of Maths, V5, 1955, pp285-309

   Answer to Trivial Exercise

    1 -- 1 --> 2 -- 1 --> 3

   needs a third arrow from 1 to 3:

    1 --------- +2 -------> 3

. . . . . . . . . ( end of section Category Theory) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see