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