A category consists of a class of objects and a class of morphisms. Examples are the category of rings with ring homomorphisms, and the category of topological spaces with continous maps as morphisms. In category theory one may express constructions of mathematics such as products (or more generally limits) and reason about them in a general setting. Category theory also provides a formal setting for reasoning about interactions between categories using the concepts of functors and natural transformations. Our main interest in category theory, however, comes from its applications to computer science and logic. In computer science for example, category theory can be used as a setting for models of programming languages.
This course will cover: Categories, functors, natural transformations, Yoneda Lemma, limits and colimits, adjunctions, monads and algebras. There will also be a short introduction to categorical logic interpreting regular logic in a regular category, and showing how to use regular logic as an internal language for reasoning about regular categories. Likewise we show how to interpret simply typed lambda calculus in cartesian closed categories. Finally, the last section of the notes is classic material on the category of complete partial orders and the solution of recursive domain equations.
There will be no real lectures, but we will meet once a week for about an hour to discuss exercises at the black board. The students are expected to read the material before the weekly meeting and to prepare a presentation of the exercises at the blackboard.
| Weekly meetings | We propose to meet at ITU Thursdays from 10. Meetings will take between one and two hours. On Thursday September 2 we meet in 4A22. The rest of the meetings will be in 4A14. Notice that by 10, we mean 10:00 (as opposed to 10:15) |
|---|---|
| Teachers | Thomas Hildebrandt and Rasmus E. Møgelberg |
| Registration | To sign up for the course, please email one of the teachers. |
| Prerequisites | Students are expected to have a good background in mathematics. However, even though applications of category theory to computer science and logic are covered in the course, a background in computer science is not necessary. |
| Notes | Basic Category Theory by Jaap van Oosten. |
| Credits | 7.5 ECTS |
| Grading | Will be based on active participation: Passed / Not-passed |
The meeting on 7/10/04 has been moved to Friday 8/10/04 12-14 in room 3A18.
By recommendation of the PhD study board, we have made the evaluation proceedure more precise. To pass the course, each student must solve an exercise at the board at least 3 times. By solving we mean that the student answers the question of the exercise and demonstrates that (s)he understands the material needed for the exercise. At least one of these exercises must be done at one of the last 4 sessions.
Carsten Butz: Regular categories and regular logic
Saunders MacLane: Categories for the Working Mathematician
Roy L. Crole: Categories for Types
| Date | Material covered | Exercises | Recommended extra exercises |
|---|---|---|---|
| 02/09/04 | Chp 1 | 1,3,5,6,8,9,12,13,14,15 | |
| 09/09/04 | 2.1, 2.2 + 2.3 to mid p. 13 | 18,21,24 + bonus | Details of examples 2.2(c,i,j) and ex 25 |
| 16/09/04 | 3.1, 3.2 | Yoneda ex., 33,36,37,47 (if time: 38) | 32,35,48 |
| 23/09/04 | 3.2, 3.3 | 51, 52, 53, 56, 46 | 39 |
| 30/09/04 | 4.1, 4.2 | 64, 65, 66, 67, 70 | 69, 62 (in particular 69!) |
| 07/10/04 | 4.3, 4.4, 4.5 | 71 (a,b,d,e), 73, 79, 80, 82 | 84, 85, 86 |
| 14/10/04 | Chp 5 (until Thm 5.2) | 89, 91, 92, 93, 97, 98 | 90, 94 |
| 28/10/04 | Chp 5+6 (until 6.1 or 6.2) | 98, 102, 103, 104 | 105, 107 |
| 04/11/04 | Chp 6 | 109, 110, 119 | 111,112 |
| 18/11/04 | Chp 7.1, 7.2 | 119, 120, 122 | |
| 25/11/04 | Chp 8 | 124, 125, 128 | 129 |
| 02/12/04 | Chp 8 | 128, 131, 132, 133 |