Mathematical Semantics of Computer Systems, MSCS (4810-1168)
Handout for Lecture 3 (2016/10/17)
Ichiro Hasuo, Dept. Computer Science, Univ. Tokyo
http://www-mmm.is.s.u-tokyo.ac.jp/∼ichiro

Video recording of the lectures is available at:
http://www-mmm.is.s.u-tokyo.ac.jp/videos/mscs2016(ask me for username, password)
We loosely follow [4], but it hardly serves as an introductory textbook. More beginner-friendly
ones include [1, 5]; other classical textbooks include [6, 2]. nLab (ncatlab.org) is an excellent
online information source.

1

Today’s Goal, ICome to understand and prove the following statement.
Proposition 1. Let X, Y ∈ C. A product of X and Y , if it exists, is unique up-to a canonicalisomorphism.

2

Today’s Agenda I

2.1

Categories, Functors

Definition. Functor
Example. Monotone functions as functors (for preorders considered as categories); monoid homomorphisms as functors (for monoids).
Example. Graphs as functors. Monoid/group actions as functors.

2.2

Reasoning with Arrows

Definition. Epi, mono. Split epi, split mono.
Definition. Coproduct.

3

Today’s Goal II

Identify the following framework of abstract interpretation [3] as an instance of adjunction. (Thanksare due to Kengo Kido for a nice introduction.)
Definition (Galois connection). Let L and L be posets; and α : L → L and γ : L → L be monotonefunctions. The pair (α, γ) is said to be a Galois connection if, for any x ∈ L and x ∈ x,α(x) ≤L x

if and only ifx ≤L γ(x) .

Example (interval domain). Let
L := P(N){}and L := {∅} ∪ [l, r] l, r ∈ N ∪ {−∞, ∞}, l ≤ rwhere each set is ordered by inclusion. Moreover,α(S) := [min S, max X] andThen the pair (α, γ) is a Galois connection.

1γ(S) := {n ∈ N | n ∈ S} .

4Today’s Agenda II

4.1

Natural Transformations

Definition. Natural transformation
Example. Natural transformations in graphs, and in monoid/group actions.
Natural transformations between monotone maps as functors.
Definition. Horizontal and vertical composition of natural transformation

4.2

Limits and Colimit

Definition. Diagram, cone, cocone
Definition. Limit, colimit
Proposition 2. Limits from products and equalizers
Corollary 1. Concrete presentation of (co)limits in Sets

4.3

AdjunctionDefinition. Homset.
Definition. Adjunction.
Example. Free monoids.
Definition. Unit, counit.
Lemma 1. Adjoint transposes by units and counits.
Proposition 3. Characterization of adjuction by: 1) the universality of η (Def. 3.2 of [Lambek &Scott], intuitive for free monoids); 2) the triangular equalities (Def. 3.1 of [Lambek & Scott]).
Lemma 2.
1. Adjoint functors determine each other uniquely up-to canonical natural isomorphisms.
2. Composition of adjoints.

4.4

Limits as Adjoints

Definition. Functor category
Proposition 4. Limits give rise to an adjunction.

5Exercises
1. Formulate and prove the following statement.
A right adjoint preserves limits.
2. Prove the following: in an adjunction F ⊣ G, G is faithful if and only if every component ofthe counit ε is an epi. [6, Thm. IV.3.1]

2

6

Report Problems
1. Prove that: in the category Sets of sets and functions, an arrow is a mono if and only if it isan injective function. Similarly, an arrow is an epi if and only if it is a surjective function.
2. Give a detailed proof of the Today’s Goal, I :Let X, Y ∈ C. A product of X and Y , if it exists, is unique up-to a canonicalcommuting isomorphism.

Reports are due at the beginning of the next lecture.

References[1] S. Awodey. Category Theory. Oxford Logic Guides. Oxford Univ. Press, 2006.
[2] M. Barr and C. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Available online.
[3] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis ofprograms by construction or approximation of fixpoints. In R.M. Graham, M.A. Harrison andR. Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252. ACM, 1977.
[4] J. Lambek and P.J. Scott. Introduction to higher order Categorical Logic. No. 7 in Cambridge
Studies in Advanced Mathematics. Cambridge Univ. Press, 1986.
[5] T. Leinster. Basic Category Theory. Cambridge Univ. Press, 2014.
[6] S. Mac Lane. Categories for the Working Mathematician. Springer, Berlin, 2nd edn., 1998.

3