Category Theory Lecture Notes

Charles Wells (Case W Reserve) 2401 1998 Dec 31 12:41:00

Informations

• Publié par: mtoledan
• Publié le: 21 novembre 2011
• Nombre de lectures: 21
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Category Theory Lecture Notes for ESSLLI Michael Barr Department of Mathematics and Statistics McGill University Charles Wells Department of Mathematics Case Western Reserve Universityc Michael Barr and Charles Wells, 1999Contents Preface iv 1 Preliminaries 1 1.1 Graphs 1 1.2 Homomorphisms of graphs 2 2 Categories 4 2.1 Basic de nitions 4 2.2 Functional programming languages as categories 6 2.3 Mathematical structures as categories 8 2.4 Categories of sets with structure 10 2.5 of algebraic structures 11 2.6 Constructions on categories 13 3 Properties of objects and arrows 17 3.1 Isomorphisms 17 3.2 Terminal and initial objects 18 3.3 Monomorphisms and subobjects 19 3.4 Other types of arrow 22 4 Functors 26 4.1 Functors 26 4.2 Actions 30 4.3 Types of functors 32 4.4 Equivalences 34 5 Diagrams and naturality 37 5.1 Diagrams 37 5.2 Natural transformations 42 5.3 between functors 46 5.4 Natural involving lists 47 5.5 transformations of graphs 48 5.6 Combining natural transformations and functors 49 5.7 The Yoneda Lemma and universal elements 50 6 Products and sums 55 6.1 The product of two objects in a category 55 6.2 Notation for and properties of products 57 6.3 Finite products 64 6.4 Sums 69 6.5 Deduction systems as categories 71 7 Cartesian closed categories 73 7.1 Cartesian closed 73 7.2 Properties of cartesian closed categories 77 7.3 Typed -calculus 79 7.4 -calculus to category and back 80 iiiiv Contents 8 Limits and colimits 82 8.1 Equalizers 82 8.2 The general concept of limit 83 8.3 Pullbacks 86 8.4 Coequalizers 88 8.5 Cocones 89 9 Adjoints 92 9.1 Free monoids 92 9.2 Adjoints 94 9.3 Further topics on adjoints 97 10 Triples 99 10.1 Triples 99 10.2 Factorizations of a triple 100 11 Toposes 102 11.1 De nition of topos 102 11.2 Properties of toposes 104 11.3 Presheaves 106 11.4 Sheaves 107 12 Categories with monoidal structure 111 12.1 Closed monoidal categories 111 12.2 Properties of A− C 114 12.3 -autonomous categories 115 12.4 Factorization systems 116 12.5 The Chu construction 117 Bibliography 119 Index 123Preface About these notes These notes form a short summary of some major topics in category theory. They are a condensation (with some rearrangement) of part of [Barr and Wells, 1999]. The chapter and section numbers in the notes are not the same as those in the book. About categories Categories originally arose in mathematics out of the need of a formalism to describe the passage from one type of mathematical structure to another. A category in this way represents a kind of mathematics, and may be described as category as mathematical workspace. A category is also a mathematical structure. As such, it is a common generalization of both ordered sets and monoids (the latter are a simple type of algebraic structure that include transition systems as examples), and questions motivated by those topics often have interesting answers for categories. This is category as mathematical structure. Finally, a category can be seen as a structure that formalizes a mathematician’s description of a type of structure. This is the role of category as theory. Formal descriptions in mathematical logic are traditionally given as formal languages with rules for forming terms, axioms and equations. Algebraists long ago invented a formalism based on tuples, the method of signatures and equations, to describe algebraic structures. Category theory provides another approach: the category is a theory and functors with that category as domain are models of the theory. Other categorical literature All of the topics in these notes are covered in more depth, with applications to computing science, in our text [Barr and Wells, 1999]. Most of the topics are also developed further, but without applications to computing science, in [Barr and Wells, 1985], [Mac Lane, 1971], [McLarty, 1992], [Freyd and Sce- drov, 1990] and [Borceux, 1994] Other texts speci cally concerning applications to computing science include [Asperti and Longo, 1991], [Crole, 1994], [Gunter, 1992], [Manes and Arbib, 1986], [Pierce, 1991], [Rydeheard and Burstall, 1988] and [Walters, 1991]. Various aspects of the close relationship between logicandcategories(intheirroleastheories)aretreatedin[MakkaiandReyes,1977],[LambekandScott, 1986], [Bell, 1988] and [Ad amek and Rosicky, 1994]. Recent collections of papers in computer science which have many applications of category theory are [Pitt et al., 1986], [Pitt, Poigne and Rydeheard, 1987], [Ehrig et al., 1988], [Main et al., 1988], [Gray and Scedrov, 1989], [Pitt et al., 1989], [Pitt et al., 1991], [Fourman, Johnstone and Pitts, 1992], [Seely, 1992], [Pitt, Rydeheard and Johnstone, 1995] and [Moggi and Rosolini, 1997]. The reader may nd useful the discussions of the uses of category theory in computing science in [Goguen, 1991], [Fokkinga, 1992] and in the tutorials in [Pitt et al., 1986]. Michael Barr Charles Wells Department of Mathematics Department of Mathematics and Statistics Case Western Reserve University McGill University 10900 Euclid Ave 805 Sherbrooke St. W. Cleveland, OH 44106-7058 Montreal, Quebec USA Canada H3P 1S4 [e-mail] [e-mail] http://www.math.mcgill.ca/~barr http://www.cwru.edu/artsci/math/wells/home.html v1. Preliminaries 1.1 Graphs The type of graph that we discuss in this section is a speci c version of directed graph, one that is well adapted to category theory, namely what is often called a directed multigraph with loops. A graph is an essential ingredient in the de nition of commutative diagram, which is the categorist’s way of expressing equations.Theconceptofgraphisalsoaprecursortotheconceptofcategoryitself:acategoryis,roughly speaking, a graph in which paths can be composed. 1.1.1 De nition and notation Formally, to specify a graph, you must specify its nodes (or objects) and its arrows. Each arrow must have a speci c source (or domain)nodeandtarget (orcodomain) node. The notation ‘f :a−!b’ means thatf is an arrow anda andb are its source and target, respectively. If the graph is small enough, it may be drawn with its nodes indicated by dots or labels and each arrow by an actual arrow drawn from its source to its target. There may be one or more arrows { or none at all { with given nodes as source and target. Moreover, the source and target of a given arrow need not be distinct. An arrow with the same source and target node will be called an endoarrow or endomorphism of that node. We will systematically denote the collection of nodes of a graphG byG and the collection of arrows 0 by G , and similarly with other letters (H has nodes H ,C has nodes C , and so on). The nodes form 1 0 0 the zero-dimensional part of the graph and the arrows the one-dimensional part. 1.1.2 Example Let G =f1;2g, G =fa;b;cg, 0 1 source(a)=target(a)=source(b)=target(c)=1 and target(b)=source(c)=2 Then we can representG as a R b - (1.1)  12 c 1.1.3 Example The graph of sets and functions has all sets as nodes and all functions between sets as arrows. The source of a function is its domain, and its target is its codomain. This is a large graph: because of Russell’s paradox, its nodes and its arrows do not form sets. 1.1.4 Example It is often convenient to picture a relation on a set as a graph. For example, let A=f1;2;3g, B =f2;3;4g and  =f(1;2);(2;2);(2;3);(1;4)g Then  can be pictured as R - - 123 (1.2) ? 4 Of course, graphs that arise this way never have more than one arrow with the same source and target. Such graphs are called simple graphs. 12 Preliminaries 1.1.5 Example A data structure can sometimes be represented by a graph. This graph represents the set N of natural numbers in terms of zero and the successor function (adding 1): succ R (1.3) 0 - 1 n The name ‘1’ for the left node is the conventional notation to require that the node denote asingleton set, that is, a set with exactly one element. One can give a formal mathematical meaning to the idea that this graph generates the natural numbers; see [Barr and Wells, 1999], Section 4.7.6. This informal idea of a graph representing a data type is the basis of the formal theory of sketches, developed in [Barr and Wells, 1999]. In particular, Section 4.7.6 of that text gives a formal mathematical meaning to the idea that the graph just given generates the natural numbers. 1.2 Homomorphisms of graphs A homomorphism of graphs should preserve the abstract shape of the graph. A reasonable translation of this vague requirement into a precise mathematical de nition is as follows. 1.2.1 De nition A homomorphism  from a graphG to a graphH , denoted  :G−!H,isa pair of functions  :G −!H and  :G −!H with the property that if u :m−!n is an arrow of 0 0 0 1 1 1 G, then  (u): (m)−! (n)inH . 1 0 0 Itisinstructivetorestatethisde nitionusingthesourceandtargetmappings:letsource :G −!G G 1 0 bethesourcemapthattakesanarrow(elementofG )toitssource,andsimilarlyde netarget ,source 1 H G and target . Then the pair of maps :G −!H and :G −!H is a graph homomorphism if and 0 0 0 1 1 1 H only if   source  = source H 1 0 G and   target  = target 1 0 H G 1.2.2 Notation of the form a : B−! C is overloaded in several ways. It can denote a set-theoretic function, a graph homomorphism or an arrow in a graph. In fact, all three are instances of the third since there is a large graph whose nodes are sets and arrows are functions (see 1.1.3) and another whose nodes are (small) graphs and arrows are graph homomorphisms. Another form of overloading is that if  :G−!H is a graph homomorphism,  actually stands for a pair of functions we here call  :G −!H and  :G −!H . In fact, it is customary to omit the 0 0 0 1 1 1 subscripts and use  for all three (the graph homomorphism as well as its components  and  ). 0 1 This does not lead to ambiguity in practice; in reading about graphs you are nearly always aware of whether the author is talking about nodes or arrows. We will keep the subscripts in this section and drop them thereafter. 1.2.3 Example IfG