INTRODUCTION TO CATEGORY THEORY
Graham Hutton
Lecture 4 - Special Constructions
INTRODUCTION
------------
Recall that a "natural_transformation" alpha : F -> G
between two functors F,G : C -> D is a total function
alpha that maps "objects" of C to "arrows" of D, with
alpha_A : FA -> GA for each A
and such that the "diagram"
alpha_A
FA ---------> GA
| |
| |
Ff | | Gf
| |
v v
FB ---------> GB
alpha_B
commutes for each f : A -> B.
Examples:
---------
rev : List -> List = reversing a list;
fla : Tree -> List = flattening a tree;
len : List -> Int = length of a list.
Functors categories:
--------------------
Functors as objects, natural transformations as arrows.
The Godement calculus:
----------------------
Pre/postcomposition with functors;
Horizontal composition;
Combinatorial properties.
This lecture:
-------------
+-----------------------------------------------------+
| Special constructions = extra categorical structure |
+-----------------------------------------------------+
ISOMORPHISMS
------------
Definition: two objects A and B are "isomorphic",
written A ~ B, if there exists two arrows f : A -> B
and g : B -> A that are each others inverses, i.e.
g o f = id_A f o g = id_B
Notes:
------
o Every arrow has "at most one" inverse. Suppose
that g and g' are both inverses of f, i.e.
g o f = id_A and f o g = id_B;
g' o f = id_A and f o g' = id_B.
Then it is easy to show that g = g':
g
= { identities }
g o id_B
= { assumption }
g o f o g'
= { assumption }
id_A o g'
= { identities }
g'
o Invertable arrows are called "isomorphisms".
Example:
--------
In the category SET, two sets are isomorphic precisely
when they have the same "cardinality", and a function
is an isomorphism precisely when it is a "bijection".
INITIAL OBJECTS
---------------
The notion of an "initial object" is a special
construction that exists within some categories.
Definition: an initial object in a category is
an object 0 such that for each object A there is
a "unique" arrow of type 0 -> A.
Notes:
------
o A category may have more than one initial object,
but they are all "uniquely isomorphic". Suppose
that 0 and 0' are two initial objects. Then, by
intiality, there exists unique arrows
f : 0 -> 0' and g : 0' -> 0
from which we can form composite arrows
g o f : 0 -> 0 and f o g : 0' -> 0'
However, by initiality,
id_0 : 0 -> 0 and id_0' : 0' -> 0'
are the unique arrows of their types, from which
we conclude that the following equations hold:
g o f = id_0 and f o g = id_0'
Hence, the unique arrows f and g establish that
0 and 0' are uniquely isomorphic.
o If they exist, we say that initial objects in a
category are "unique up to a unique isomorphism"
(i.e. categorically indistinguishable), and often
speak of "the" rather than "an" initial object.
Examples:
---------
o For the categories SET and REL, the empty set {}
is the unique initial object. For any set A,
the unique function or relation of type {} -> A
is simply the empty function or relation.
o For a pre-ordered set interpreted as a
category, an initial object is precisely a minimal
element of the underlying set, i.e. an element a
in A such that for all b in A. a <= b.
TERMINAL OBJECTS
----------------
Many constructions in category theory can be dualised
by "turning all the arrows around". The dual of an
initial object is called a "terminal object".
Definition: a terminal object in a category is
an object 1 such that for each object A there is
a "unique" arrow of type A -> 1.
Note: A category may have more than one terminal
object, but they are all "uniquely isomorphic".
Examples:
---------
o For the category SET, any one-element set {*} is
a terminal object. For any set A, the unique
function of type A -> {*} is the constant function
that simply returns * for all arguments.
Note: there is a one-to-one correspondance between
the functions of type {*} -> A and the elements of
the set A. More generally, for any category with
a terminal object 1, the arrows of type 1 -> A are
sometimes viewed as the "elements" of the object A.
o For the category REL, the unique initial object {} is
also the unique terminal object. More generally, REL
is an example of a "self-dual" category.
PRODUCTS
--------
The categorical notion of a "product" generalises
the set-theoretic notion of a product.
Definition: a product of two objects A and B in
a category is a triple
where
AxB is a "product" object;
pi_0 : AxB -> A is a "left projection" arrow;
pi_1 : AxB -> B is a "right projection" arrow
such that for each object C and pair of arrows
f : C -> A and g : C -> B
there is a unique "split" arrow f^g : C -> AxB
that makes the following diagram commute:
C
/ . \
/ . \
/ . \
f / f^g \ g
/ . \
/ . \
v v v
A <---- AxB ----> B
pi_0 pi_1
Definition: a category "has products" if every
pair of objects in the category has a product.
Notes:
------
o Unique arrows that make a diagram commute are
usually denoted by dashed or dotted arrows.
o pi_0 and pi_1 are "destructors" for products,
while the ^ operator is a "constructor".
o The above diagram states that for any triple
that "looks like" a product, there is a
unique arrow f^g that factorises the look-a-like
product in terms of a real product.
o There may be more than one product object for two
objects, but they are all "uniquely isomorphic".
Examples:
---------
o The category SET has products, with the set AxB
defined as the Cartesian product of A and B,
AxB = {(a,b) | a in A and b in B}
and the remaining components defined as follows:
pi_0 (a,b) = a
pi_1 (a,b) = b
(f^g) (c) = (f c, g c)
o A pre-ordered set interpreted as a category
has products precisely when every pair of elements
a,b in A has a "maximal lower bound" in A, i.e. an
element axb in A that is a lower bound for a and b,
axb <= a ^ axb <= b
and is maximal among all such lower bounds:
forall c in A. c <= a ^ c <= b => c <= axb
Universality:
-------------
Formally, the defining commuting diagram for a
product states that equivalence
pi_0 o h = f ^ pi_1 o h = g <=> h = f^g
holds for all h : C -> AxB. This equivalance is
known as the "universal property" of ^, and is
the key to proving properties of products.
Derived properties:
(1) pi_0 o f^g = f
(2) pi_1 o f^g = g
(3) (pi_0 o h) ^ (pi_1 o h) = h
(4) (foi) ^ (goi) = f^g o i
Proofs:
For (1) and (2) simply substitute the RHS of the
universal property into the LHS; for (3) do the
opposite. For (4), we calculate as follows:
f^g o i = (foi) ^ (goi)
<=> { universal property of ^ }
pi_0 o f^g o i = foi ^ pi_1 o f^g o i = goi
<=> { properties (1) and (2) }
f o i = f o i ^ g o i = g o i
<=> { reflexivity }
true
Product arrows:
---------------
Definition: if f : A -> B and g : C -> D are
arrows in a category with products, then fxg :
AxC -> BxD is the "product arrow" defined by
fxg = (f o pi_0) ^ (g o pi_1)
Derived properties:
(5) id_A x id_B = id_AxB
(6) (f o g) x (h o i) = (f x h) o (g x i)
(7) pi_0 o (fxg) = f o pi_0
(8) pi_1 o (fxg) = g o pi_1
(9) (fxg) o h^i = (foh) ^ (goi)
For example, (5) can be verified as follows:
id_A x id_B = id_AxB
<=> { definition of x }
(id_A o pi_0) ^ (id_B o pi_1) = id_AxB
<=> { identities }
pi_0 ^ pi_1 = id_AxB
<=> { universal property of ^ }
pi_0 o id_AxB = pi_0 ^ pi_1 o id_AxB = pi_1
<=> { identities }
pi_0 = pi_0 ^ pi_1 = pi_1
<=> { reflexivity }
true
Note: the typing rule for product arrows together
with (5) and (6) states that x is a "bifunctor".
CO-PRODUCTS
-----------
The dual of a product is called a "co-product", and
generalises the set-theoretic notion of a "sum".
Definition: a co-product of two objects A and
B in a category is a triple
where
A+B is a "co-product" object;
iota_0 : A -> A+B is a "left injection" arrow;
iota_1 : B -> A+B is a "right injection" arrow;
such that for each object C and pair of arrows
f : A -> C and g : B -> C
there is a unique "join" arrow fvg : A+B -> C
that makes the following diagram commute:
C
^ ^ ^
/ . \
/ . \
f / fvg \ g
/ . \
/ . \
/ . \
A ----> A+B <---- B
iota_0 iota_1
Definition: a category "has co-products" if every
pair of objects in the category has a co-product.
Notes:
------
o iota_0 and iota_1 are "constructors" for co-products,
while the v operator is a "destructor". We can
think of v as a "case" operator.
o The above diagram states that for any triple
that "looks like" a co-product, there is a
unique arrow fvg that factorises the look-a-like
co-product in terms of a real co-product.
o There may be more than one co-product object for two
objects, but they are all "uniquely isomorphic".
Examples:
---------
o The category SET has co-products, with the set A+B
defined as the disjoint sum of A and B,
A+B = {(0,a) | a in A} U {(1,b) | b in B}
and the remaining components defined as follows:
iota_0 a = (0,a)
iota_1 b = (1,b)
(fvg) (0,a) = f (a)
(fvg) (1,b) = g (b)
o The category REL has co-products, with the set A+B
defined as in SET, and the remaining components
defined as relations in the obvious way. Moreover,
co-products in REL are also products in REL (!).
o A pre-ordered set interpreted as a category
has co-products precisely when every pair of elements
a,b in A has a "minimal upper bound" in A.
Universality:
-------------
Formally, the defining commuting diagram for a co-
product states that equivalence
h o iota_0 = f ^ h o iota_1 = g <=> h = fvg
holds for all h : A+B -> C. This equivalance is
known as the "universal property" of v.
Derived properties:
(1) fvg o iota_0 = f
(2) fvg o iota_1 = g
(3) (h o iota_0) v (h o iota_1) = h
(4) (iof) v (iog) = i o fvg
Co-product arrows:
------------------
Definition: if f : A -> B and g : C -> D are
arrows in a category with co-products, then f+g
: A+C -> B+D is the "co-product arrow" defined by
f+g = (iota_0 o f) v (iota_1 o g)
Derived properties:
(5) id_A + id_B = id_A+B
(6) (f o g) + (h o i) = (f + h) o (g + i)
(7) (f+g) o iota_0 = iota_0 o f
(8) (f+g) o iota_1 = iota_1 o g
(9) hvi o (f+g) = (hof) v (iog)
Note: the typing rule for co-product arrows together
with (5) and (6) states that + is a "bifunctor".