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.
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.
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:
Then add two more (quickly) to the other two sides of the triangle:
Here is a complete list of all the morphisms:
You had to add both b-1->c and a-3->c at quickly because in a category each pair of adjacent arrows
Two complete the category we must give the rule for composing adjacent labels. Normal addition will do in this little category:
I will abbreviate this
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.
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.
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:
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:
Note. Some use "n:X->Y" for X-n->Y. This would be ambiguous in MATHS.
So we have a set of relations:
So we write can a path of alternating boxes and arrows (objects and morphisms) out like this
and mean
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
so that,
Notice the abuse of notation:
and so on. In other words the category defines the rules of composition of the morphisms.
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:
We often omit the'(X)' when this is clear from the context:
The identity has the important property of not changing morphisms when composed with them:
This will be defined formally below.
We can define an abreviation 'mo(X,Y)` for the set of morphisms connecting X with Y:
All objects have identities:
We can show that there can be no more than one Identity morphism per object. First define the generic forma of an identity.
Hence the uniqueness of Id(X) for all X.
Hence we can prove that each object has a monoid:
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.
. . . . . . . . . ( end of section Examples) <<Contents | End>>
The diagram commutes if for all different paths with the same end points define the same morphisms:
a
X---->Y
\ |
\c |b
\ |
\ |
\V
Zwhere 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--->CodAnd with equal objects aligned vertically [ Figure 1 ] below.
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--->Zwe can use the diagrams to assert properties in a fairly obvious way.
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
}.
a
W----->X
| |
|c |b
| |
V d V
Y----->Z
. . . . . . . . . ( end of section Examples of Commutative_Diagrams) <<Contents | End>>
. . . . . . . . . ( end of section Diagrams) <<Contents | End>>
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
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.
for X,Y:C, X isomorphic Y::@=isomorphisms(C)& mo(X,Y), there are isomorphisms connecting X and Y.
Some write C^op for dual(C).
(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).
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.
for C:category, zero_objects(C) ::=initial_objects(C) & terminal_objects(C).
A-f->X-m->Y
A-g->X-m->Y
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,
f in C(Y,\alpha) iff
for all i
Y-f(i)->\alpha(i)
f in C(\alpha,Y) iff
for all i
\alpha(i)-f(i)->Y
For all i
P-pr(i)->\alpha(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->Pand for all i
Y-------f(i)->\alpha(i)
Y-p->P-pr(i)->\alpha(i)
Products can also be given a categorial construction as a terminal object in a different category:
(Pr4): For all I,α,some th (PRODUCT(P=> ><α)).
In typeset/written documentation a prefixed "><" is shown as a large capital "Π".
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.
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:
Y<-(\/f)-(\/X)<-i.inj-X(i)
Y<--------f(i)--------X(i))
all c<------g--a-------f------->b
some c--v--->r<------------u-----b
all c----k-------->s<---h-------b
one r--t-->s[click here if you can fill this hole]
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.
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->d2Examples:
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
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 ><.
?? replace '->' by other arrows...in FUNCTORIALITY? [click here if you can fill this hole]
. . . . . . . . . ( end of section An Alternate Basis) <<Contents | End>>
See ... [click here if you can fill this hole]
Similarly we can define entire and simple relations and maps as relations that are entire and simple:
. . . . . . . . . ( end of section Allegories) <<Contents | End>>
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.
Compare Σ.algebra in [ math_43_Algebras.html ]
\psi(A)--\psi(f)-->\psi(B)----\gamma----->B
\psi(A)-----\delta-------->A--f---------->B
Notice that
Dually - \psi.coAlg in Categories.
Fixed points of functors are universal algebras!
Notice that
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
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 [ Gunter92 ] covers the theory in detail.
. . . . . . . . . ( end of section Fixed Points of Functors) <<Contents | End>>
[click here if you can fill this hole]
1 -- 1 --> 2 -- 1 --> 3needs a third arrow from 1 to 3:
1 --------- +2 -------> 3
. . . . . . . . . ( end of section Category Theory) <<Contents | End>>
(Gunter92): Carl A Gunter, Semantics of Programming Languages:Structures and
Techniques, The MIT press Cambridge MA 1992
(LehmanSmith81): Lehman & Smith 81, D J Lehmann & M B Smyth, "Algebraic specification of data types", Math Systems Theory V14, 1981, pp97-139
(ManesArbib86): Manes & Arbib 86, Manes & M Arbib,Algebraic Approaches to Program Semantics, Springer Verlag Monograph 1986
(Tarski55): Tarski 55, A Tarski, "A Lattice Theoretical Fixed point Theorem and its Applications," Pacific Journal of Maths, V5, 1955, pp285-309
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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see