Mathematical Semantics of Computer Systems, MSCS (4810-1168)
Handout for Lecture 5 (2016/10/31)
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)

Part I: Adjuction (ctn’d)
1

Today’s Goals

1.1

Goal I: Abstract Interpretation via Adjunction

Identify the following framework of abstract interpretation [3] as an instance of adjunction. (Thanks
are 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 if x ≤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]and γ(S) := {n ∈ N | n ∈ S} .

Then the pair (α, γ) is a Galois connection.

1.2

Goal II: Quantifiers via Adjunction (à la Lawvere)

Let f : X → Y be a function, and 2X and 2Y be the posets of predicates over X and Y , respectively,
whose orders are the inclusion order.
We think of the posets 2X and 2Y as categories. Then we have two adjunctions∃f2X o⊥⊥∀f

2

Today’s Agenda

2.1

Adjunction

Definition. Homset.
Definition. Adjunction.

1f −1# Y2<.

(1)

Example. Free monoids.
Definition. Unit, counit.
Lemma 1. Adjoint transposes by units and counits.
Proposition 1. 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.

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

2.3

Limits as Adjoints

Definition. Functor category
Proposition 3. A limit gives rise to an adjunction.

3Exercises
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]

Report Assignments
Deadline: at the beginning of the next lecture.
1. Let (E, e) be an equalizer in the situation Ee/Xfg// Y . Prove that the arrow e isnecessarily a mono.
2. Let X × Y denote a product of X and Y ; and 1 be a terminal object. Prove that there exist
the following canonical isomorphisms.
∼=(a) (X × Y ) × Z →X × (Y × Z)∼=(b) 1 × X →XPart II: the Yoneda Lemma
Remember: we loosely follow [4], but it hardly serves as an introductory textbook. More beginnerfriendly ones include [1, 5]; other classical textbooks include [6, 2]. nLab (ncatlab.org) is anexcellent online information source.

2

4

Today’s Goal

Familiarize yourself with the Yoneda lemma. Identify it as a category theory analogue of the Cayleyrepresentation theorem:
Theorem (Cayley). Every group G is isomorphic to a subgroup of π(|G|).

5Today’s Agenda

5.1

Equivalence of Categories

Definition. Subcategory, faithful functor, full functor
Lemma 3. Any functor preserves isomorphisms.
A full and faithful functor reflects isomorphisms.
Definition. Equivalence of categories
Proposition 4. Equivalence from a full, faithful and iso-dense functor.

5.2

The Yoneda Lemma

Definition. Covariance, contravariance
Theorem (Yoneda). The Yoneda lemma, the Yoneda embedding as a full and faithful functor
Definition. end, coend
Theorem. The Yoneda lemma, the (co)end form
Lemma 4. Ends as limits [6, Prop. IX.5.1]
Lemma 5. Homfunctors preserve (co)limits, hence also (co)ends

6

Exercises
1. Formulate the “naturality” of the Yoneda correspondence)(Nat C( , X), F ∼= FX
and prove it.

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