Homomorphisms, Bilimits and Saturated Domains (Some Very Basic Domain Theory)

Paul Taylor

March 1987

Abstract

The most powerful feature of categories of posets with directed sups is the ability to solve domain equations such as D ≅ D^{D}. A crucial ingredient of this technique is the fact that for certain kinds of diagrams (in particular sequences of “projection pairs”) the limit and colimit are isomorphic. This much is known to everyone in the subject: what appears not to be generally known is

(i) that we only use the fact that the maps are adjoint (not that they are respectively epi and mono) and

(ii) what the corresponding results for other limits (such as pullbacks) are.

I propose to set out the basic definitions and results here, introducing the following terms:

(i) homomorphism, for a continuous map with a left adjoint (projections being a special case),

(ii) comparison, for this left adjoint (embeddings being a special case),

(iii) bilimit, for the common limit and colimit of filtered diagrams of homomorphisms,

(iv) bifinite, for a domain expressible as a bilimit of finite posets and

(v) saturated, for a domain of which any other is a retract.

I shall justify my strongly-held view that the last two should replace the existing terms “profinite” and “universal”.

We begin by recalling the basic ideas of the domain-theoretic solution of equations such as D ≅ D^{D}, and showing that homomorphisms (not just projections) arise frequently. We look briefly at general limits and colimits and explain the difference between bifinite and profinite posets. Then the proof of the limit-colimit coincidence for cofiltered diagrams of homomorphisms is given. Working with cofiltered diagrams is cleaner and no more difficult than working with sequences. Although the case for sequences of projections is sufficient for solving domain equations, this general form arises naturally from “indexed retracts”. We then seek limits of other kinds of diagrams of special classes of maps, in particular pullbacks and simply-connected limits of projections. Finally we apply this to finding saturated domains.

Introduction

I am going to take it for granted that the reader knows that a cpo is a partially ordered set with a least element (⊥) and directed joins or sups (written ^{⋁↑}) and that a continuous map is a function between the underlying sets of two cpos which preserves (the order and) directed sups but not necessarily bottom. I personally prefer the term “ipo” (inductive partial order) as used in [Plotkin 1976] since (i) these are precisely the posets for which every monotone endofunction has a least fixed point, (ii) I expect more of something called “complete” than merely directed sups and (iii) the term “complete category” is clearly not available for the obvious generalisation. However since I have harder axes to grind regarding other terminology, I shall here stick to the commonly used name.

Write CPO for the category of cpos and continuous maps. It is also convenient to consider posets with directed sup but not necessarily bottom, again with continuous maps; we shall not bother to name these (Reynolds calls then predomains and Gunter calls them dcpos, using the term dcppo instead of cpo), but just write V for the category.

I shall use a semi-colon (;) for right-handed composition in a category, so f ; g : A → C is the composite of f : A → B and g : B → C. [Arbib & Manes 1975] is probably sufficient for the category theory we use; otherwise the reader is referred to [Mac Lane 1971]. The new [Lambek & Scott 1986] is much to be recommended.

The importance of projection pairs was recognised early in the development of the subject. By this we mean a pair of continuous maps i : X ↣ Y (the embedding) and p : Y ◁ −X (the projection) with the following properties:

(i) i ⊣ p (i is left adjoint to p), i.e.

\frac{ix ≤ y}{x ≤ py}

bijectively for x ∈ X, y ∈ Y; equivalently 1_{X} ≤ i; p and p; i ≤ 1_{Y}.

(ii) i is injective (1–1 or mono) and p is surjective (onto or epi); equivalently (given (i)) i;p = 1_{X}.

One of these three inequalities is of course redundant and the definition is usually given in terms of the other two; the reason for this presentation is that we wish to drop condition (ii).

There are two major traditional reasons for interest in projection pairs, namely in order to make the function-space construction functorial in its first argument and because it is for diagrams of these maps that the limit-colimit coincidence holds. We shall show here that for both of these we may drop the surjectivity condition. A third reason, as shown in [Taylor 1986], is that (with the same extension) this is the only satisfactory class of substitution maps for indexed domains; we shall not attempt to discuss this topic here.

It is a basic and inescapable fact that the function-space construction is contravariant in the first argument. In other words, to convert a function X → Y to one X′ → Y′ we need maps X′ → X and Y → Y′:

[figure: X; Y; X′; f; Y′; g]

so that [− → −] : C^{op} × C → Set. The analogous result in logic is that a stronger condition is satisfied less often.

Since we wish to solve domain equations involving function-spaces we need a way of dealing with expressions involving function-spaces and variables. For reasons I shall not spell out here, in order to do this we need to make the function space covariant in the first argument. This is standardly done by providing maps in both directions, so we put D ⊂ C^{⇆} and define [− → −] : D ×D → D in the obvious way. It has been customary to restrict the class D of pairs of maps to the projection pairs. This is a red herring. We should use homomorphisms instead.

What makes it possible to solve such equations is that we may take the limit, lim X^{i}, of the diagram

[figure: ⋯; F^{3}ϵ^{X}; F^{3}X; F^{2}ϵ^{X}; F^{2}X; F ϵ^{X}; F X; ϵ^{X}; X]

The reason for using F ϵ^{X} and not ϵ^{F X} is that when we apply F to the whole diagram we get the same diagram back (but shifted along one), so lim F X^{i} = lim X^{i}. Hence if F preserves limits of this kind, i.e. F (lim X^{i}) ≅ lim F X^{i}, we have F (lim X^{i}) ≅ lim X^{i}. Writing F^{∞}X = lim X^{i}, we have a fixed point (up to isomorphism) of the functor F.

Observe that this construction depends on ϵ^{X} as well as the functor F and the “seed” X, unlike the poset version of this argument (Tarski’s theorem) where there is only one instance of the order relation anyway. For the direct analogue of that result we may put X = {⊥}, the one-point cpo, in which case ϵ^{X} is uniquely determined; then we have the final fixed point of F (unfortunately this gives the trivial solution to D ≅ D^{D}). Since we only use ϵ^{X} and not ϵ^{F^{n}X}, we only really need the map ϵ^{X} : F X → X and not a natural transformation (“copointed endofunctor”) ϵ : F ⇒ id.

Exercise [1] Let ϵ^{X} : F X = X^{X}◁ −X by f ↦ f⊥, and write 2 for the two-point lattice • → •. Show that ϵ^{F 2} ≠ F ϵ^{2}; indeed they are incomparable in [(2^{2})^{(2^{2})} → (2^{2})]. Hint: see [Stoy 1977], page 114.

In order to solve D ≅ D^{D} we need the pairs of maps, and also that the limit be preserved. The latter follows because (by definition of lim and colim) [colim X_{i} → lim Y^{j}] ≅ lim^{ij}[X^{i} → Y^{j}] and the fact that for a diagram of projection pairs the limit of the projections is isomorphic to the colimit of the embeddings.

Often it is more intuitive to look at the comparisons instead, especially in the case of an embedding η_{X} : X ↣ F X where we think of X as a subset of F X. A particular example of this arises in Denotational Semantics. Suppose we have a language with certain constructors (say two unary and one binary operator and some atoms); we want to form the domain of expressions in these constructors, possibly with some holes. This leads us to an equation of the form E = F (E)_{⊥} (where in the example F (X) = A + X + X + X × X), with seed η : {⊥} ↣ F ({⊥})^{⊥}. In this case η_{X} is only defined for X = {⊥}, so again we see we have to use F^{n}η_{X} and not η_{F^{n}X}. In terms of comparisons, F^{∞}X is an initial fixed point.

Since the foregoing motivation was standard literature fifteen years ago, we shall not discuss recursive domain equations further. In the next section we introduce homomorphisms, and show that they arise naturally in Domain Theory not just as projections. The remainder of the paper is devoted to more formal proofs of results.

First we look at general limits of continuous functions in CPO and V. This is instructive both as a convenient setting for subsequent calculation and also as an indication of the relationship between domains and more general kinds of topological spaces. Then we prove the limit-colimit coincidence in V, generalising not only from projections to homomorphisms but also from sequences to filtered diagrams; this latter extension disposes of a lot of unnecessary but common tergid notation without any increase in difficulty. Finally we investigate limits of other kinds of diagrams of homomorphisms (in particular pullbacks) and conclude with an application to the construction of saturated (“universal”) domains.

There are no new domain equations which can be solved with homomorphisms rather than projections, and indeed the limit-colimit coincidence for homomorphisms can be derived quite easily from that for projections. The homomorphism from the bilimit to a term in the diagram factors as a projection followed by an injective homomorphism; the diagram of projections drives the bilimit, whereas the injective homomorphisms give rise to closures on the terms (which can be derived directly from the diagram as the directed sup of the closures to other terms) which simply serve to discard part of the information they provide. Nevertheless the ordered retracts example (and the indexed domain theory to which it leads) needs the full form, and I personally prefer clean concise proofs with precisely the right hypotheses.

This does not necessarily mean the most general form: [Plotkin & Smyth 1982], for instance, considers “O-categories” (enriched over posets with countable ^{⋁↑}). However the additional generality of this approach is potentially spurious. If we insist on regarding the symbols in categorical calculus as ranging over sets in a very classical “bag of sand” sense, then clearly the O-category case is separate; but if in stead we regard them as varying over objects in a cartesian-closed category (as is consistent with our use of them), then the generalisation is immediate by inspection. On the other hand, dealing with O-categories makes the proof untidy, especially if, as Gordon Plotkin and Michael Smyth are accustomed to do, everything is introduced as a sequence. Anyway, that’s the point of view of a mathematician rather than a computer scientist.

1 Homomorphisms and Comparisons

A homomorphism of domains is a continuous function h : Y → X possessing a left adjoint c (which is necessarily continuous and uniquely determined by h). I have two justifications for the use of this term. First, restricted to continuous lattices (see [Day 1975] and [Gierz et al. 1980]) it gives precisely the maps preserving the (^{⋁↑}, inf) operations for which continuous lattices are the algebras. Secondly, homomorphisms turn out to be the only satisfactory choice of substitution maps for indexed domains [Taylor 1986]. The term was introduced independently in [Gunter 1985] and [Taylor 1986]. The left adjoint of a homomorphism is called a comparison.

Write CPO^{hm} and CPO^{cp} for the categories of cpos and respectively homomorphisms and comparisons, so CPO^{hm} ≅ (CPO^{cp})^{op}. In fact we also have duality at the 2-level, since for two homomorphisms h ≤ h′, the corresponding comparisons have c′ ≤ c. The same superscripts may be used for other categories of domains, such as continuous lattices, boundedly complete countably based algebraic lattices (sometimes known as Scott domains) and countably based bifinite cpos (hitherto known as SFP domains).

Examples 1.1 Let X, Y ∈ V. The the following pairs are respectively comparisons and corresponding homomorphisms:

(a)  x ←x x ↦ cx  X◁ −c(X)  c is a coclosure on X
(b)  cy ←y y ↦ y  c(Y) ↪ Y  c is a closure on Y
(c)  (x, ⊥) ←x (x, y) ↦ x  X × Y ◁ −X  Y has ⊥
(d) x_{1} ⋎ x_{2} ←(x_{1}, x_{2}) x ↦ (x, x)  X ↪ X × X  X is a lattice
(e)  (x, x) ←x (x_{1}, x_{2}) ↦ x_{1} ⋏ x_{2} X × X◁ −X X is boundedly complete
(f)  Kx ←x f ↦ f⊥  X^{X}◁ −X  X has ⊥
(g) \{ \begin{matrix}x ←x \\ ⊥_{X} ←⊥_{new} \end{matrix}  x ↦ x  X ↪ X_{⊥}  X has ⊥
(h)  x ←x \{ \begin{matrix}x ↦ x \\ y ↦ ⊥ \end{matrix}  X ⊕ Y ◁ −X  X and Y have ⊥
(i)  likewise  X +_{⊥} Y ≅ X_{⊥} ⊕ Y_{⊥}◁ −X_{⊥}

Identities and composites of homomorphisms (respectively comparisons) are also homomorphisms (respectively comparisons). Beware that the ↪ symbol above means an injective homomorphism, not an injective comparison (embedding). We shall use the terms coembedding and coprojection for an injective homomorphism and its corresponding surjective comparison, although I think they are somewhat unsatisfactory.

The above examples are all either epi or mono, so apart from ad hoc composition of them we have not seen a naturally occurring homomorphism which is neither.

Exercise [2] Let Λ be a cpo model of the λ-calculus, such as Pω, D_{∞}, T^{ω} or one of the saturated domains which we shall construct later. Let A, B ∈ Λ be types (idempotents) as in [Scott 1976] with A ≤ B. Then A; B ⊣ B ; A gives a homomorphism from B to A. [Hint: show that A; B, B; A, A; B; A and B; A; B are idempotent and exhaust the composites, and investigate the order relation among them.]

This explains the term comparison: a map which arises from an instance of the order relation. [Taylor 1986] shows how comparisons in a category of domains are analogous to the order relation inside domains themselves.

There is, however, a sense in which epis and monos do account for all homomorphisms, in that we have a factorisation result:

Proposition 1.2 Let h : Y → X be a homomorphism of domains with corresponding comparison c : X → Y. The h factors as a projection Y ◁ −I followed by a coembedding I ↪ X. There is a closure c; h on X and a coclosure h; c on Y whose images are isomorphic to I. Moreover every isomorphism between the images of a closure and of a coclosure arises uniquely in this way. □

It is easy to show that any epi or mono homomorphism arises up to isomorphism from some instance of the order relation between idempotents, so if we require all isomorphisms to be comparisons by fiat we have precisely the maps which arise in this way.

The following are worth noting:

CPO^{cp}(X, 2)^{op} ≅ CPO^{hm}(2, X) ≅ \{ \begin{matrix}X & if X has ⊤ \\ ∅ & otherwise \end{matrix}

where the comparison corresponding to x ∈ X, which we write as [x], is the characteristic function of X \ ↓ x, and the homomorphism takes ⊥ and ⊤ to x and ⊤ respectively.

CPO^{hm}(X, 2)^{op} ≅ CPO^{cp}(2, X) ≅ X_{fp}

where the homomorphism corresponding to x ∈ X_{fp} is the characteristic function of ↑ x, and the comparison takes ⊥ and ⊤ to ⊥ and x respectively. These show that CPO^{hm}(X, Y) may be any poset, not necessarily a cpo like CPO(X, Y).

The original reason for introducing projection pairs was to make the function space functorial, i.e. to extend the object part of the construction to the morphisms of a category. Of course we can do this with homomorphisms as well, the category being CPO^{hm}.

Exercises Show that the following type-expressions give rise to functors (V^{hm})^{n} → V^{hm} for appropriate values of n:

[3] product, X × Y

[4] function-space, [X → Y] or Y^{X}

[5] lifting, X_{⊥} = X ∪ {⊥_{new}}

[6] amalgamated sum (with ⊥ identified), X ⊕ Y on CPO

[7] coproduct (disjoint sum), X + Y

[8] separated sum (with new bottom), X +_{⊥} Y = (X + Y)_{⊥} ≅ X_{⊥} ⊕ Y_{⊥}

[9] Smyth powerdomain, P_{S}X

[10] Hoare powerdomain, P_{H}X

[11] Plotkin powerdomain, P_{P} X

From the point of view of solving domain equations such as D ≅ D^{D}, we are also interested in natural transformations. The examples previously given of homomorphisms provide examples of natural transformations between functors of the above kind. We use “dropping a variable”, f ↦ f⊥ : X^{X}◁ −X, to solve D ≅ D^{D}.

Exercise [12] Show that proposition 1.2 fails for categories because in general adjunctions need not be idempotent. However (using the same notation) there is a category Z whose objects are arrows x → hy in X (with x ∈ X, y ∈ Y), or equivalently cx → y in Y, such that the forgetful functors give a factorisation of h the opposite way into a coembedding followed by a projection. Hence the argument that all maps with continuous right adjoint should be considered to be comparisons still holds.

2 Limits

Recall that a cone over a diagram d : I → C with vertex X is a family ϕ^{i} : X → d(i) for i ∈ I such that for every arrow u : i → j in I we have ϕ^{j} = ϕ^{i} ; d(u). ϕ is limiting if, given any other cone g^{i} : Y → d(i), there is a unique mediating map g : X → Y with g^{i} = g ; ϕ^{i}. The vertex of the limiting cone is called the limit and, being unique up to isomorphism, is written lim^{i∈I} d(i). There are dual terms cocone and colimit(ing).

Lemma 2.1 Let d : I → V be any diagram of posets with^{⋁↑} and continuous maps. Then the limit, lim^{i∈I} d(i), exists in V and consists of compatible families, ⟨x^{i} : i ∈ I⟩ such that d(u)(x^{i}) = x^{j} for all u : i → j in I, with the componentwise order. The limiting cone is given by the component projections and the mediating map for the cone g^{i} : X → d(i) is given by x ↦ ⟨g^{i}(x) : i ∈ I⟩. Proof We calculate directed sups componentwise because d(u) is continuous. Likewise it is easy to verify that the component projections are continuous and yield a cone, also that f is continuous and uniquely determined as the mediating map. □

We have used nothing about filteredness, homomorphisms or bottom in this result, and we shall see in due course what the effects of omitting these conditions are. We may speak of “limits” without mention of the ambient category because

Proposition 2.2 Let C be a full subcategory of V containing some non-discrete domain and d : I → C any diagram. If d has a limit lim_{i∈I}^{C} d(i) in C then it is the limit in V, i.e. the mediating map ϕ : L = lim_{i∈I}^{C} d(i) → lim_{i∈I}^{V} d(i) = X in V is an isomorphism. Proof Let u, v ∈ U ∈ C with u < v. Let x ∈ X; we must show that there is a unique l ∈ L with ϕ(l) = x. Since L is the limit in C, let f : U → L be the mediating map for the cone ! ; ⌜x⌝ ; π^{i} : U → 1 → X → X^{i}. Put l = f(u), so ϕ(l) = x. If ϕ(l′) = x then Kl′ satisfies the defining property of f so f = Kl = Kl′. Hence l is the unique preimage of x. Now let x ≤ y in X; we have to show that ϕ^{−1}(x) ≤ ϕ^{−1}(y) in L. Let s : U → 2 by w ↦ ⊥ iff w ≤ u, so s(u) = ⊥ and s(v) = ⊤. Consider the cone s; ⌜x ≤ y⌝; π^{i} : U → 2 → X → X^{i} and let f : U → L be the mediating map. This is continuous, so ϕ^{−1}(x) = f(u) ≤ f(v) = ϕ^{−1}(y). Hence ϕ is bijective and reflects order, whence it is an isomorphism. □

Exercises

[13] Find a parallel pair of maps in CPO whose equaliser does not have ⊥.

[14] Let C be a full subcategory of CPO with products. If the exponential X^{Y} exists in C then it is [Y → X] from CPO.

[15] Let C^{n} be the “flat domain” with 2^{n} maximal points, together with bottom. Consider the diagram with vertices the C^{n} and maps C^{n+1} → C^{n} which identify the maximal points in pairs. The limit topological space of this diagram is obtained by lifting (i.e. adding ⊥ to) the Cantor space. However this topology is coarser than the Scott topology, which is discrete on the maximal points.

[16] Find a parallel pair in BiPos_{f} whose equaliser is an algebraic but not bifinite cpo. [Hint (Gunter): to the standard example which has a pair with infinitely many mubs, add two extra points; then consider the pair which send them both to each, fixing the rest.]

3 “Bifinite” versus “Profinite”

It is established usage to call an object which can be expressed as a limit of finite objects profinite. For instance profinite groups are of importance because by the Galois correspondence the limit of finite groups corresponds to the colimit of finite algebraic field extensions, and so profinite groups arise as Galois groups of possibly infinite algebraic extensions. Gunter [1985] adopted the term for Plotkin’s SFP domains, which we call bifinite; apparently this was suggested to him by Scott. However I wish to discourage this usage.

Galois theory provides a duality between arithmetic (fields) and geometry (groups). Analogously we have a duality between topology (domains) and logic (distributive lattices). Specifically, the spectrum (space of prime ideals) and compact-open set lattice provide a duality between the categories of finite spaces (posets or domains) and finite distributive lattices. Since any distributive lattice is ind-finite, i.e. a colimit of finite distributive lattices, this duality extends to one between profinite posets and distributive lattices, where by profinite I mean its strict interpretation in a category whose morphisms are all continuous maps.

The characterisation of profinite posets as totally order-separated compact Hausdorff spaces was first made by [Speed 1972]; this topology is the Lawson or patch topology. Giving the finite posets a topology which relates to their order leads to the coherent topology on the profinite objects (this is not in general the Scott topology). [Johnstone 1983], pp 72–75 and 246–251, gives a full description.

The exercises of the preceding section illustrate profinite posets which are not bifinite. It may be argued that the use of the word profinite follows that of homomorphism, in which case Gunter’s usage is justified. However I believe that the whole of Coherent Logic (which is, after all, only PROLOG with disjunction) will be needed in due course in Computer Science, and so the term profinite should be reserved for the established (more general) concept. The forthcoming [Vickers 1988] argues along these lines, and so although this claim has yet to be fully justified, it would be embarrassing if when it is the necessary word is no longer available.

4 Colimits

Colimits also exist in V, although they are harder to describe. Given a diagram d : I → V we construct the colimit in six stages:

(i) First take the disjoint union U = ⋃ |d(i)| of the underlying sets.

(ii) Identify elements of U as necessary for compatibility with the diagram, so if x = d(u)(y) for x ∈ d(i), y ∈ d(j) and u : j → i then we identify x with y. Notice that this entails many more identifications via “zig-zags”. Write U/R for the quotient set; this is the colimit in Set.

(iii) Impose the preorder on U/R so that [x] ≺ [y] whenever x ≤ y in some d(i). Transitivity makes many more instances of this because of the new identifications from (ii); this is the colimit preorder.

(iv) Quotient the preorder (U/R, ≺) by the equivalence relation (≺)∩(≻) to get a poset (U/S, ≤) (S is a coarser equivalence relation); this is the colimit in Pos.

(v) Adjoin ^{⋁↑} to get Idl(U/S, ≤). The ideals may as well be represented by the union of the S-equivalence classes, so are still subsets of U, now under inclusion.

(vi) Quotient the ideals as forced by continuity of the colimiting cocone; we may do this by closing the sets in (v) under directed joins from d(i). This gives the colimit L in V.

Proposition 4.1 V has colimits. Proof Let us begin by being more precise about the foregoing construction. The points of the colimit may be represented as subsets of ⋃|d(i)|, or alternatively as families of subsets α_{i} ⊂ d(i). These are closed under the following conditions (corresponding to those above):

(i)

(ii) If x = d(u)(y) for x ∈ d(i), y ∈ d(j) and u : j → i then x ∈ α_{i} iff y ∈ α_{j}.

(iii) If x′ ≤ x ∈ α_{i} then x′ ∈ α_{i}; the order is now by inclusion.

(iv) Inclusion is automatically antisymmetric

(v) and has directed joins.

(vi) if x = ^{⋁↑} x^{j} and x^{j} ∈ α_{i} then x ∈ α_{i}.

Write ⟨x⟩ for the closure of {x} ⊂ d(i) under these conditions.

The colimiting cocone takes x ∈ d(i) to ⟨x⟩, and the colimit consists of directed joins of such ⟨x⟩. The values taken by another cocone f_{i} at ⟨x⟩ form a set with greatest element f_{i}(x) which is independent of the choice of generator x; moreover this value is continuous in x. Hence the mediating map is defined, unique and continuous. □

The subsets α_{i} are Scott-closed by conditions (iii) and (v), and form a compatible family under d(u)^{−1} by condition (ii). We are therefore interested in the limit of the lattices of closed sets. Not every compatible family arises, however, only those generated under directed sup from the ⟨x⟩. These are irreducible: if p ⊂ a ∪ b for p ∈ L and a, b and compatible families of closed sets then either p ⊂ a or p ⊂ b. In fact not every irreducible closed set occurs either.

The lattice of Scott-open sets of a cpo X is in fact isomorphic to [X → 2], and by the definition of colimits, [colim X_{i} → 2] ≅ lim[X_{i} → 2]. Hence we know what the Scott topology of the colimit is (the lattice of closed sets is opposite).

Given the topology on a space we can try to recover the space. The closure of a point is an irreducible closed set and for cpos if one point is below another then its closure is contained in that of the other. Since the Scott topology on a cpo is T_{0} this correspondence with closed sets distinguishes the points. A space in which every irreducible closed set is the closure of a unique point is said to be sober. This technique of transferring attention from points to open (or closed) sets is called the theory of locales; for a comprehensive introduction see [Johnstone 1983], which in particular gives an example of a non-sober cpo.

We can, however, say that the colimit of a diagram of cpos is a certain subspace of the space of points of the limit of the corresponding diagram of Scott topologies and inverse image maps. This subspace consists of the images of the points of the terms of the diagram, together with directed joins. This problem seems to me a good reason for restricting attention to sober cpos (in fact algebraic⇒continuous⇒sober) or moving to locales. As with limits, we need not worry about mentioning the category with respect to which colimits are defined.

Proposition 4.2 Let C be a full subcategory of CPO containing a non-discrete domain and d : I → C a diagram. If d has a colimit L in C then the mediating map ϕ : X → L, where X is the colimit in CPO, factors through the natural map from X to its sobrification. Proof Let u < v ∈ U ∈ C as before and s = ⌜u < v⌝ : 2 → U. We aim to show that ϕ^{∗} : [L → 2] → [X → 2] is bijective and hence an isomorphism of Scott topologies. For V ⊂ X open, let χ^{V} : X → 2 be the characteristic function and f : L → U the mediating map for the cone ι_{i} ; χ^{V} ; s : X^{i} → X → 2 → U. The function g : L → U by l ↦ u if f(l) ≤ u and v otherwise is continuous and satisfies the defining property of f, so this describes f. Also if W ⊂ L with ϕ^{−1}(W) = V then h : L → U by l ↦ v if l ∈ W and u otherwise also satisfies the property. Hence f^{−1}(v) is the unique such W. L and X therefore have the same topology, so since they are both T_{0}, L contains X and is contained in its sobrification. □

Exercise [17] Show that the directed sups and the problems with sobriety still arise even for finite diagrams.

5 Proof of the Limit-Colimit Coincidence for CPO

We have given a completely explicit description of limits and an almost explicit description of colimits of cpos and shall now turn to the phenomenon of their isomorphism. We prefer to proceed from the limit to the colimit. Observe carefully the distinction between (co)limits of homomorphisms or comparisons in V^{hm} (or V^{cp}) and in V.

We shall work with (co)filtered diagrams rather than sequences. Filtered diagrams are the categorical generalisation of directed sets. A category I is filtered if

(i) it is nonempty

(ii) for any two objects i, j ∈ I, there is an object k ∈ I and two morphisms i → k and j → k

(iii) for any two objects i, j ∈ I and morphisms u, v : i ⇉ j, there is an object k ∈ I and a morphism w : j → k with u; w = v ; w.

The third condition does not arise for posets; nor does it arise for categories if all of the maps in the category are mono, as is the case for diagrams of embeddings. A filtered diagram is a functor d : I → C from a filtered category. Dually cofiltered. It avoids confusion if we refer to the objects and morphisms of a diagram category like I as points and arrows.

Let d : I → V^{hm} be a cofiltered diagram of homomorphisms with limit (quâ continuous maps) L = lim^{i∈I} d(i) and limiting cone π^{i} : L → d(i). For u : i → j in I write h^{u} = d(u) : d(i) → d(j) for the homomorphism and c_{u} : d(j) → d(i) for its left adjoint (comparison).

Lemma 5.1 For i ∈ I, π^{i} is a homomorphism. Proof Given x ∈ d(i), we have to find the least compatible family ⟨y^{j}⟩ with x ≤ y^{i}. For j ∈ I, choose u : k → i and v : k → j by cofilteredness. Since ⟨y^{j}⟩ is to be a compatible family, we must have x ≤ y^{i} = h^{u}(y^{k}), so since c_{u} ⊣ h^{u}, c_{u}(x) ≤ y^{k}. Again using compatibility, h^{v}(y^{k}) = y^{j}, so h^{v}[c_{u}(x)] ≤ y^{j}.

Now let u′ : k′ → i, v′ : k′ → j be another choice. Again using cofilteredness (first to choose a point with arrows to both k and k′, then to choose an arrow into this making the composites equal), let w : l → k and w′ : l → k′ be such that u′′ = w;u = w′;u′ : l → i and v′′ = w;v = w′;v′ : l → j. Then c_{u′′} ; h^{v′′} = c_{u} ; c_{w} ; h^{w} ; h^{v} ≥ c_{u} ; 1 ; h^{v}, so h^{v′′}[c_{u′′}(x)] bounds h^{v}[c_{u}(x)] and h^{v′}[c_{u′}(x)].

Now I claim that y^{j} = ^{⋁↑}{h^{v}[c_{u}(x)] : u : k → i, v : k → j} gives a compatible family. We have to check that y^{j′} = h^{w}(y^{j}) for w : j → j′. Since h^{w} preserves ^{⋁↑} and h is functorial, we have only to consider the sets

{h^{v;w}[c_{u}(x)] : u : l → i, v : l → j} ⊂ {h^{v′}[c_{u}(x)] : u : k → i, v′ : k → j′}

where the inclusion holds by postcomposition with w. By a similar argument as before using filteredness, we can choose l → k, l → j in order to find a point of the smaller set above any chosen point in the larger. The directed sups are therefore equal. The foregoing argument shows that ⟨y^{j}⟩ is the least compatible family with x ≤ y^{i}, and so automatically the adjoint exists and is continuous (indeed preserves all sups). □

Write ι_{i} ⊣ π^{i} and ρ_{i} = π^{i} ; ι_{i}, but do not suppose from this choice of notation that we have a projection pair. However

Lemma 5.2 If the h^{u} are projections, then so are the π^{i}. Proof c_{w} ; h^{w} = 1_{d(k)}, so h^{v′′}[c_{u′′}(x)] = h^{v}[c_{u}(x)] and y^{j} is also equal to this. In particular π^{i}[ι_{i}(x)] = y^{i} = x, so ι_{i} ; π^{i} = 1_{d(i)} as required. □

Lemma 5.3 ⟨ι_{i}⟩ is a cocone for the diagram of comparisons. Proof Since the πs form a cone, π^{j} = π^{i} ; h^{u}. Now a diagram of left adjoints commutes iff the corresponding diagram of right adjoints commutes, so it follows immediately that ι_{j} = c_{u} ; ι_{i} for all u : i → j as required. □

Lemma 5.4 ^{⋁↑} ρ_{i} = 1_{L} Proof Clearly ρ_{i} ≤ 1_{L}. Let ⟨y^{j}⟩ ∈ L be a compatible family. Then for i ∈ I let x = y^{i} and ⟨z^{j}⟩ = ι_{i}(x) be the least compatible family with x ≤ z^{i}. Then of course y^{i} = x ≤ z^{i} ≤ y^{i} so y^{i} = π^{i}[ι_{i}(y^{i})]. Then π^{i}⟨y^{j}⟩ = π^{i}[ρ_{i}⟨y^{j}⟩] ≤ π^{i}[^{⋁↑}_{k} ρ_{k}⟨y^{j}⟩] ≤ π^{i}⟨y^{j}⟩. In this we have componentwise equality, so ⟨y^{j}⟩ = ^{⋁↑}_{k} ρ_{k}⟨y^{j}⟩ as required. □

Lemma 5.5 ⟨ι_{i}⟩ is a colimiting cocone for the diagram of comparisons quâ continuous maps. Proof Let ϕ_{i} : d(i) → X be another cocone for this diagram. We need ι_{i}; ϕ = ϕ_{i} for all i ∈ I so ϕ = ^{⋁↑} π^{i}; ι_{i}; ϕ = ^{⋁↑} π^{i}; ϕ_{i} by lemma 5.4. It’s easy to see that this is continuous and the unique mediating map. □

Lemma 5.6 Let q_{ij} be directed in each suffix. Then ^{⋁↑}_{ij} q_{ij} = ^{⋁↑}_{k} q_{kk}. □

(This is the lemma used to prove that componentwise continuity suffices for continuity on a binary product).

Lemma 5.7 ⟨π^{i}, ι_{i}⟩ is a limiting cone for the diagram of homomorphisms quâ homomorphisms. Proof Let g^{i} : X → d(i) be a cone of homomorphisms and f_{i} : d(i) → X the corresponding cocone of comparisons. Since L is the colimit we have a unique mediating map f : L → X with f_{i} = ι_{i}; f, and since it is the limit we also have unique continuous g : X → L with g^{i} = g; π^{i}. We have to use 1_{d(i)} ≤ f_{i} ; g^{i} and g^{i} ; f_{i} ≤ 1_{X} to show 1_{L} ≤ f ; g and g ; f ≤ 1_{X}.

By lemma 5.6, ^{⋁↑}_{ij} π^{i};ι_{i};f;g;π^{j};ι_{j} = ^{⋁↑}_{k} π^{k};ι_{k};f;g;π^{k};ι_{k}. By lemma 5.4, the left-hand side of this is f ; g, whilst the right-hand side is ^{⋁↑} π^{k} ; f_{k} ; g^{k} ; ι_{k} ≥ ^{⋁↑} π^{k} ; 1_{d(k)} ; ι_{k} = 1_{L}. Conversely g ; f = ^{⋁↑} g ; π^{i} ; ι_{i} ; f = ^{⋁↑} g^{i} ; f_{i} ≤ 1_{X}. □

Lemma 5.8 If we have a diagram of projections, and a cone of projections over it, then the mediating map is a projection. Proof Equality holds in the calculation of f ; g. □

Theorem 5.9 For any filtered diagram of homomorphisms, the limit of the homomorphisms quâ continuous functions, the colimit of the comparisons quâ continuous functions and the limit of the homomorphisms quâ homomorphisms exist and are naturally isomorphic. Proof It only remains to formulate and prove naturality. This is left as an exercise [18]. □

We say that L is the bilimit of the diagram.

Exercises

[19] Show that each of the functors given as examples before preserves bilimits. Such a functor is said to be continuous.

[20] Show that Idl (which gives the poset of ideals of a domain) and Cocl (which gives the poset of coclosures) are not continuous functors.

[21] Show that for a cone of homomorphisms ⟨f_{i}, g^{i}⟩ we have ^{⋁↑} g^{i} ; f_{i} = 1 iff the mediating homomorphism g is mono (a coembedding).

6 Limit-Colimit Coincidence for Other Categories of Domains

We now have the result for CPO. In order to extend it to other categories of domains, we need only show that properties such as continuity (or algebraicity), being countably-based and lattice conditions are preserved by cofiltered limits of homomorphisms.

Lemma 6.1

(a) Comparisons preserve ≪ and compactness.

(b) Embeddings also reflect them. Proof

[a] Let c : X → Y be a comparison with right adjoint h and x_{1} ≪ x_{2} in X. Suppose c(x_{2}) ≤ ⋁↑ y_{i} in Y; then by adjointness and since h is continuous, x_{2} ≤ ^{⋁↑} h(y_{i}) in X. By hypothesis we now have x_{1} ≤ h(y_{i}) for some i, and using adjointness again we have c(x_{1}) ≤ y_{i} as required. x ∈ X is compact iff x ≪ x.

[b] Easy exercise [22]. □

Proposition 6.2 A bilimit of continuous (algebraic) posets is continuous (respectively algebraic). Proof Let ⟨y^{i}⟩ ∈ bilim X^{i}. By lemma 6.1 and since ι_{i}(y^{i}) ≤ ⟨y^{j}⟩,

{ι_{i}(x) : x ∈ X^{i}, x ≪ y^{i}} ⊂ {x : x ∈ bilim X^{i}, x ≪ ⟨y^{i}⟩}

(both sets being directed) so in order to show that ⟨y^{i}⟩ is ≪-approximated it suffices to show that it is the join of the smaller set. But ⟨y^{i}⟩ = ^{⋁↑} ι_{i}(y^{i}) by the previous section and y^{i} = ^{⋁↑}{x : x ∈ X^{i}, x ≪ y^{i}} by continuity of X^{i}. Similarly for algebraic. □

Proposition 6.3 A countable bilimit of countably-based domains is countably based. Proof The proof is the same: we take the (countable) union of the (countable) approximating sets. □

Proposition 6.4 A bilimit of domains with any of the following properties also has that property:

(a) lattice

(b) boundedly complete

(c) L-domain [Jung 1987]: every principal lower set is a continuous lattice.

(d) SFP [Plotkin 1976]: every finite set of finite elements is contained in a finite mub-closed set of finite elements.

Proof

[a,b,c] These properties say that the algebraic operations of (a) arbitrary, (b) non-empty and (c) connected meet exist. Algebraic operations in a limit are inherited from the terms, so long as the maps in the diagram are homomorphisms for them, and homomorphisms in our sense are.

[d] A subset is mub-closed if it contains all minimal upper bounds for subsets of it, and every bound (in the ambient set) of such a subset lies above a minimal upper bound for it. The SFP property is inherited by a directed union of sets of finite elements. □

Exercise [23] Exhibit a diagram of complete lattices and continuous maps whose limit is not a lattice.

A domain is a bilimit of finite posets iff it is algebraic and satisfies the last of these properties; we call such a domain bifinite. The prefix “bi” is intended for use in any 2-category for bilimits and objects which can be expressed as bilimits of special objects, just as we have, for instance, procyclic groups such as the p-adic numbers.

7 Other Limit-Colimit Coincidences

The phenomenon of the limit of a diagram being naturally isomorphic to the colimit of the same kind of diagram did not arise first in Domain Theory but in Linear Algebra. The categorical product and coproduct of finitely many vector spaces are isomorphic, usually being called their direct sum (written ⊕) because the dimensions add. [The symbol ⊗ is used for the tensor product because the dimensions multiply.] This limit-colimit coincidence is one of the defining properties of an Abelian category [Mac Lane 1971].

Where CPO has the limit-colimit coincidence for filtered diagrams and Abelian categories have it for finite ones, CSLat (complete [semi]lattices and ⋀-preserving maps) has it for all of them. By the Adjoint Functor Theorem, a function has a left adjoint iff it preserves ⋀. This preserves ⋁, which is ⋀ on the opposite lattices. We therefore have a duality CSLat ≅ CSLat^{op} which takes a lattice to its opposite and a ⋀-homomorphism to its adjoint.

Theorem 7.1 Let d : I → CSLat be any diagram of complete semilattices and π^{i} : L → d(i) its limiting cone. Then ι_{i} : d(i)^{op} → L^{op} is the colimiting cone of the diagram c : I^{op} → CSLat of adjoints. □

There is an intermediate example which to some extent unifies these. Abelian groups and semilattices are special cases of commutative monoids, namely with the additional axioms of invertibility and idempotence respectively.

Theorem 7.2 The product and coproduct of any finite collection of commutative monoids are naturally isomorphic. Proof Define δ_{i}^{j} : X^{i} → X^{j} to be the identity if i = j and the zero map (which takes everything to the unit of the commutative, associative operation) otherwise. Taking the limit over j we then have a map ι_{i} : X^{i} → L and as before ρ_{i} = π^{i}; ι_{i}. Just as we had ^{⋁↑} ρ_{i} = 1_{L} before, we now have ∑^{i} ρ_{i}(x) = x for x ∈ L. (In fact the category of commutative monoids, like CPO, has an internal hom, and is a symmetric monoidal-closed category with tensor product ⊗). We show that ι_{i} is a colimiting cocone precisely as before. Again formulation and proof of naturality are exercises [24]. □

Exercise [25] Why is commutativity necessary?

It is this result which justifies the use of matrices. A homomorphism between two direct sums is given by an array of homomorphisms between the respective components. ρ_{i} is the matrix with a single 1 in the i^{th} place on the diagonal.

It is only possible to define the contravariant map (adjoint) in the idempotent (lattice) case (unless perhaps we could do something with adjoint matrices), so the result does not extend to nondiscrete diagrams such as pullbacks. With some work we may extend the notion of a commutative monoid to the infinite case and hence generalise the CSLat example. We see, therefore, that

the limit-colimit coincidence arises from the similarity of a category to its objects

The Scott limit-colimit coincidence generalises to categories with an initial object and filtered colimits. We call these inductive categories and write I for the 2-category of them. I^{cp} is then itself a (large) inductive category, so the similarity has now become very close, but not as close as we would want it. Some of the theory of inductive categories is a straightforward rewriting of the cpo case, but there are many new subtleties and complications, so this is beyond the scope of this paper.

A rival form of domain theory, originally due to Berry [1977], has recently been popularised by Girard [1985, 1986] and discussed further in [Coquand, Gunter & Winskel 1986,7] and Lamarche [1987]. As well as directed joins we have pullbacks (meets of pairs bounded above), these being preserved by the maps (stability). In fact these pullbacks should really be connected limits, but the strong finiteness condition obscures the codirected meets. Remarkably, this category is cartesian closed, although the order relation on the function-space is not pointwise.

In the early parts of this paper we emphasised general adjoint pairs of maps, but in the stable case it turns out that these are forced to be embedding-projection pairs. Once again the category of stable domains and rigid embeddings resembles its objects (having directed joins and connected meets) and has a limit-colimit coincidence.

For a more abstract case let C^{re} be the category of retraction-pairs in an arbitrary category C, i.e. ⟨p, i⟩ with i; p = 1. Writing lim, colim and bilim for the limit of the surjections, the colimit of the injections and the limit in C^{re} respectively, we have

Proposition 7.3

[a] If lim and bilim both exist then they are isomorphic.

[b] Likewise for colim and bilim.

[c] If lim and colim both exist and are isomorphic then so does bilim (and is isomorphic to them).

[d] The existence of bilim does not imply that of lim or colim, even in the presense of the other. Proof

[a] Let π^{i} : lim → X^{j} and (i_{i}, p^{i}) : X^{i} → bilim be the limiting cones. By the universal property of lim there is a comparison map p : bilim → lim in C with p; π^{i} = p^{i}. Put ι_{i} = i_{i} ; p, then ι_{i} ; π^{i} = 1 so ⟨ι_{i}, π^{i}⟩ are C^{re}-maps, and they form a cone in C^{re}. But bilim is universal, so we have a comparison map (ι, π) : bilim → lim in C^{re} with i_{i} ; ι = ι_{i} = i_{i} ; p and π ; p^{i} = π^{i}. Then π; p; π^{i} = π; p^{i} = π^{i} so π; p = 1 by the universal property of lim. Since ⟨ι, π⟩ form a retract, ι; π = 1 also and π has inverses on both sides and hence is an isomorphism.

[b] The same argument in C^{op}.

[c] Put bilim = lim = colim with limiting cones i_{i} : X^{i} → colim and p^{j} : lim → X^{i}. Then (i_{i}, p^{i}) : bilim → X^{i} is limiting.

[d] ContLat^{pr} and ContLat have products, but the latter does not have coproducts. □

This result is intended as suggestive of ways of showing that limits of diagrams of pairs do not exist other than as bilimits, since V has all limits and colimits, rather as we showed that limits and colimits in categories of domains and continuous maps are those from V. It does not answer all such questions, since we have assumed that (ι_{i}, π^{i}) is a valid pair and used the fact that it is a retraction. Perhaps there is some way of using our requirement that the function-space be functorial and continuous to prove this result another way. However we shall not pay any further attention to distinctions of in which category we have the limit.

Exercise [26] Find a subcategory D ⊂ C^{⇆} for which the above results fail.

8 Carrable Maps

CPO does not have all finite limits, so what are the maps against which we can pull back any map with the same codomain? Such maps are called carrable (French, means squarable). In fact we shall show that projections (not homomorphisms this time) provide a class of display maps [Taylor 1986] for CPO, which we need for studying indexed domain theory and hence polymorphism.

Proposition 8.1

(a) A continuous map p : X → Y between cpos is carrable iff it is a projection.

(b) The pullback of a carrable map is carrable.

(c) The composite of two carrable maps is carrable.

(d) Any terminal projection is carrable. Proof We already know what the pullback must look like in V.

[a,⇒] If p : X → Y is carrable let y ∈ Y and take the pullback against the corresponding ⌜y⌝ : 1 ↪ Y. This is the inverse image of y in X and has to have a least element, which we call iy. We now have to show that iy ≤ x iff y ≤ px; but since y = p(iy), “only if” is trivial. Let y ≤ px; consider the map 2 → Y by ⊥ ↦ y, ⊤ ↦ px and let Z be the pullback. Z has a least element, ⟨⊥, iy⟩, say, and in particular this is less than ⟨⊤, x⟩, so iy ≤ x. p therefore has a left adjoint monotone function, and this then has to preserve all, not just directed, sups.

[⇐] Let p : X◁ −Y be a projection and f : Z → Y any continuous function. Let W = X ×_{Y} Z be the pullback in V. ⟨i(f⊥_{Z}), ⊥_{Z}⟩ is the least element.

[b,c] are standard properties of pullbacks. We note that the left adjoint to the pullback-projection X ×_{Y} Z → Z is z ↦ ⟨i(fz), z⟩.

[d] Terminal maps are projections because of ⊥; they are carrable because we have products. □

Exercises

[27] The pullback of a coembedding against a coembedding is a coembedding; equivalently the intersection of the images of two closure operators is the image of a closure operator. [Hint: compose them repeatedly.] What does this say about pushouts of coprojections?

[28] The intersection of the images of two coclosure operators on a bifinite poset is another, but the result does not generalise. [Hint: consider mub-closed sets.] Apply this to pullbacks of embeddings and pushouts of projections.

[29] The pullback of a coembedding against a projection need not be a coembedding [Hint: the five-point domain which is not boundedly complete gives a counterexample].

[30] The pullback of a projection from a lattice against an embedding need not have ⊤ [Hint: try the four-point lattice 2^{2}].

[31] Likewise bounded completeness may be destroyed, contrary to the claims of [Taylor 1985] [Hint: there’s a seven-point counterexample].

[32] Continuity and bifiniteness may be created or destroyed. [Taylor 1986] gives counterexamples.

[33] The mediating map for a cone over the pullback need not be a projection. [Hint: the left adjoint to the diagonal Δ : X → X × X must be ⋎.]

Exercises The corresponding results for pushouts.

[34] A map is cocarrable in CPO iff it is strict, i.e. preserves ⊥.

[35] The pushout of an embedding against any continuous map is an embedding. [Hint: stick close to the definition of a pushout, using the dual construction to the above.]

[36] The pushout of X and Y into which Z is embedded is given by the union of X and Y with the two copies of Z identified. [Hint: x ≤ i(qy)]

[37] The pushout of a coprojection against an embedding need not be a coprojection [Hint: there’s a three-point counterexample].

9 General Limits of Projections

We have already seen that mediating maps for pullbacks are not homomorphisms. The case for most other diagrams is worse. It would appear that unless I is equivalent to a tree then there is some way of using it to calculate the equaliser of π^{0}, π^{1} : X × X ⇉ X. This equaliser is the diagonal, Δ : X → X × X, which has a left adjoint (∨) iff X is a complete lattice. Fortunately we only need trees to construct saturated domains.

Lemma 9.1 Any diagram of cpos and surjective continuous functions (in particular any diagram of projections) has a limit cpo. Proof We construct the limit in V using lemma 2.1. Since surjective maps preserve ⊥, ⟨⊥⟩ is a compatible family for the diagram and hence in the limit; it is easily seen to be the least element. □

What interests us in order to make saturated domains is when the maps in the limiting cone are split epi, i.e. when the cpos in the diagram are retracts of the limit. A particular case of this is when the limiting cone consists of projections, generalising the question of when a pullback of a projection is a projection. It turns out that there is a simple positive answer to this.

Suppose we have an embedding ι_{i} : d(i) ↣ L of a point in the diagram into the limit; then of course it has components ι_{i}^{j} : d(i) → d(j): how can we construct them? Well the most naïve answer (almost) works: take the composite of a path of projections and embeddings in the diagram (so we are allowed to go backwards as well as forwards along the arrows). Taking a detour via and embedding and returning by its projection makes no difference, but the other way round reduces the function, so just consider paths which are irredundant in this sense, or alternatively those which are maximal in the order relation on functions. We shall say that a diagram is simply connected if there is a unique irredundant (or maximal) path between any two points.

Exercise [38] Reformulate this as a condition on I alone, using the notions of equivalence of diagrams (any cone over a subdiagram may be extended uniquely to one over the whole diagram) and trees (in the undirected graph theoretic sense of having a unique path between any two points).

Lemma 9.2 Let d : I → CPO^{pr} be a simply connected diagram of cpos and projections and i, j, j′ ∈ I with j → j′. Then ι_{i}^{j} ; d(j → j′) = ι_{i}^{j′} (i.e. ι_{i}^{j} is a cone) and π^{i}; ι_{i}^{j} ≤ π^{j}, where π^{i} is the limiting cone. Proof Follows easily from the above discussion about detours. □

Proposition 9.3 Let d : I → CPO^{pr} be a simply connected diagram of cpos and projections. Then the limiting cone consists of projections. Proof The previous two lemmas guarantee that the limit exists and that we have a cone. We have only to check that π^{i} : L → d(i) and ι_{i} : d(i) → L are a projection-embedding pair, and these two calculations have just been done. □

Exercise [39] Can you show that the simple connectivity condition is necessary, either for a particular diagram d : I → CPO^{pr} or for the category I?

We want to apply this to other categories of domains, and so we want to simplify the condition of having simply connected limits. In fact what we need is (bilimits and) pullbacks of projections, so let C be a full subcategory of CPO closed under these. The reduction is of course demonstrated by a piece of graph theory. We call a category I a tree if it is non-empty and for any two points i, j ∈ I there is a unique (possibly empty) sequence of nonidentity arrows in alternate directions between them. Clearly any (diagram over a) tree is simply connected, and in fact a tree is a poset.

Exercises

[40] Any simply connected diagram is equivalent to a diagram over a tree which is at most as big.

[41] Any tree is the filtered union of its finite subtrees.

Lemma 9.4 Let I be a finite tree and J the full subcategory obtained by deleting the points with precisely one incoming arrow (i.e. a non-identity arrow through which any other factors). Then

(a) J is a tree, and

(b) J ⊂ I is an equivalence of diagrams.

Moreover unless J is a singleton,

(c) J has a point i with no incoming arrows and a unique outgoing arrow u : i < j

(d) and a point k with no incoming arrows and an arrow v : k < j. Proof Exercise [42]. □

Lemma 9.5 C has limits of finite simply connected diagrams of projections. Proof Let d : I → C^{pr} be such a diagram. The proof is by induction on the number of points: the result for a singleton is trivial, by the exercise w.l.o.g. the diagram is a tree and lemma 9.4 allows us further simplification. Then we may add a point l and arrows l → i, l → k. We extend a d : I → C^{pr} to I ∪ {l} by putting e(l) = d(i) ×_{d(j)} d(k); by proposition 9.1 the d(l → i) and d(l → k) are projections, and by hypothesis on C the pullback is in C.

The extension is an equivalence of diagrams. i and j now have a unique incoming arrow, and so their deletion yields an equivalent diagram K, which is a tree with fewer vertices than the original I. Hence by the induction hypothesis the limit of K → C^{pr} exists and the limiting cone consists of projections. By the equivalences the same holds for I ∪ {l} and I. □

Lemma 9.6 Let d : I → V^{pr} be as before and J a subtree of I; then the mediating map between the limits is a projection. Proof Let K be obtained from I by adjoining a new point l and arrows j → l for j ∈ J. Extend d to K by letting its value at l be the limit over J and at arrows j → l the projections of the limiting cone. Then I ⊂ K is an equivalence and K is simply connected. The required mediating map is part of the limiting cone over K and so is a projection by proposition 9.3. □

Theorem 9.7 Let C be a full subcategory of V closed under bilimits and pullbacks of projections. Let I be a tree and d : I → C^{pr} a diagram of projections. Then the limit exists in C and the limiting cone consists of projections. Proof Let J be the poset of finite subtrees of I under reverse inclusion, so J is a cofiltered category. Define e : J → C^{pr} as follows. Let e(J) be the limit over the finite tree J, which exists in C by lemma 9.5. If J is a subtree of J′, so we have an arrow u : J′ → J in J, let e(u) be the mediating map between the limits, which is a projection by lemma 9.6. e extends d because we may include I in J as the singleton subtrees, and I ⊂ J is an equivalence. e : J → V^{pr} is now a cofiltered diagram of projections and so has a bilimit in C, and the (bi)limiting cone consists of projections. Restricting to I gives the required result. □

Theorem 9.8 Similarly if C is closed under bilimits and pushouts of embeddings then it has colimits of simply connected diagrams of embeddings. □

Exercise [43] Is there a mediating map between limits of projections and colimits of embeddings? If so, which way does it go, and when is it invertible?

10 Saturated Domains

We now have the machinery required to construct a saturated domain. Let Σ be a countable class of finite cpos which is closed (up to isomorphism) under retracts and pullbacks of projections.

Examples 10.1 Σ may be

(a) All finite lattices

(b) All finite cpos with the property that if a subset is pairwise bounded then it has a least upper bound

(c) All finite boundedly-complete posets

(d) All posets with ⊥

(e) All L-domains, i.e. posets for which ↓ x is a lattice

whose underlying sets are finite subsets of ℕ. In (b) we may replace “pairwise” by an n-fold condition.

Consider the chains of projections in Σ, i.e. the finite sequences (X^{i})

X^{n}◁ −X^{n−1}◁ − ⋯ ◁ −X^{1}◁ −X^{0} = 1

where n is the length and X^{n} the end of the chain. Let I be the category of chains, where (X^{i}) → (Y^{i}) if the length, n, of X is at most that of Y, and for 0 ≤ i ≤ n X^{i} = Y^{i} (and the projections also coincide).

Lemma 10.2 I is simply connected (§9). Proof Easy. □

Define a diagram d : I → V^{pr} by mapping a diagram to its end and an arrow to the corresponding homomorphism from the end of the longer to that of the shorter.

Lemma 10.3 Λ = lim^{i∈I} d(i) can be expressed as a countable bilimit of Σ-domains. Proof In the previous section we showed how to construct this limit as a bilimit of pullbacks, and Σ is closed under pullbacks. It is easy to check countability. □

Lemma 10.4 Any countable cofiltered diagram is equivalent to one over ω^{op}. Proof Enumerate the points and arrows and use cofilteredness to choose points successively which have maps to the given points and equalising the given pairs of arrows. □

Proposition 10.5 Any countable bilimit of Σ-domains can be expressed as a coclosure on Λ. Proof By lemma 10.4 the bilimit may as well be an infinite sequence. Taking its initial (or rather, final) segments gives a diagram of (finite) chains, i.e. in I. The limiting cone from Λ consists of projections by the previous sections, and in particular this gives a cone over our sequence. Since this is a cofiltered diagram the mediating map is a projection. The domain is therefore a coclosure of Λ. □

Theorem 10.6 The categories of countably-based algebraic posets which are (a) lattices, (b) pairwise-bounded-complete, (c) bounded-complete, (d) SFP and (e) L-domains have saturated domains. Proof Apply proposition 10.5 to examples 10.1a–d. □

If Σ is closed (up to isomorphism) under exponentiation then Λ_{Λ} ◁ Λ and so Λ carries the structure of a model of the λβ-calculus.

Exercise [44] Perform the analogous calculation with colimits of embeddings.

11 “Saturated” versus “Universal”

The term universal domain has, in my opinion, been extremely misleading. There is nothing unique about the result of the foregoing construction. More seriously than non-uniqueness is nonfunctoriality: we have yet another example of a construction which accounts for the object but not morphism parts of a definition. In short, “universal” domains have been an excuse for failure to discuss the category of domains.

Exercises

[45] Pω is a distributive lattice.

[46] Λ = Pω ∪ {∗}, where ⊥ < ∗ < ⊤ but no other new order relations hold, is a saturated domain for ContLat_{ω}.

[47] Λ is a non-distributive lattice [Hint: if a is an element of a distributive lattice then there is at most one b with a ⋎ b = ⊤ and a ⋏ b = ⊥].

The term “saturated” has been adopted from Model Theory. We say that a model M realises a set of formulae Γ in free variables x⃗ if there is some assignment m⃗ of elements of M to the variables x⃗ such that Γ[x⃗ := m⃗] is true in M. Then M is saturated if it realises any collection of formulae of a certain kind. Given a finite poset P = {p^{0}, p^{1}, ..., p^{k}} with p^{0} = ⊥^{P} and a cpo X, there is a set Γ^{P} of coherent sequents which says that the assignment x⃗ is the image of p⃗ under an embedding P ↣ X. Specifically Γ^{P} is

⊤ ⊢ x^{0} ≤ x
⊤ ⊢ x^{i} ≤ x^{j}  whenever p^{i} ≤ p^{j}
x^{i} ≤ x^{j} ⊢ ⊥  whenever p^{i} ≰ p^{j}
x^{i} ≤ x ∧ x^{j} ≤ x ⊢ x^{m^{1}} ≤ x ∨ ... ∨ x^{m^{r}} ≤ x where {p^{m^{1}}, ..., p^{m^{r}}}
is the set of mubs of {p^{i}, p^{j}}

Then X realises ∀x.Γ^{P} iff P can be expressed as a coclosure on X. A saturated domain in our sense is then saturated in the model-theoretic sense for a certain class of formulae.

Rather a lot of discussion has been based on the accidental existence of a closure operator in Pω which fixes precisely the closure operators. Many authors have considered this an adequate candidate for a “type-of-types”. Indeed it can be used to show that certain toy polymorphic languages are consistent. However since it is only a type of types and not of terms it is unable to deal fully with dependent-type expressions.

Exercise [48!] For a given small category of domains C, construct a saturated domain Λ, and an element V ∈ Λ such that V ∈ ∥V∥ ⊂ Idem(Λ) and if A ∈ C and X : A → C^{cp} is continuous then there is some A ∈ ∥V∥ representing A and some X : A → I making the notation X(a) unambiguous.

Such a thing I might begin to consider worthy of the name “type-of-types”. [Taylor 1988], which includes an application of the general limit-colimit coincidence as we have proved it here to ordered retracts and discusses polymorphism in both the domain theory we have been discussing and the new Berry-Girard style, constructs some kind of type-of-types.

Bibliography

M.A. Arbib and E.G. Manes

[1975] Arrows, Structures and Functors — the Categorical Imperative, Academic Press

G. Berry [1978] Stable Models of Typed λ-Calculi, Proc ICALP, Springer LNCS 62 72–89

Th. Coquand, C.A. Gunter and G. Winskel

[1986] DI-domains as a model of polymorphism, Univ. Cambridge Computer Lab. technical report 107

[1987] Domain-Theoretic Models of Polymorphism, idem 116 A. Day

[1975] Filter Monads, Continuous Lattices and Closure Systems, Canad. J. Math. 27 (1975) 50–59 J.-Y. Girard

[1985] The System F of Variable Types, Fifteen Years Later, Theor Comp Sci

[1986] Lambda Calcul Typé, unpublished lecture notes C.A. Gunter

[1985] Profinite Solutions for Recursive Domain Equations, Ph.D. dissertation, University of Wis-

consin at Madison G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove and D.S. Scott

[1980] A Compendium of Continuous Lattices, Springer P.T. Johnstone

[1982] Stone Spaces, CUP Studies in Advanced Mathematics 3 C.P.J. Koymans

[1984] Models of the Lambda Calculus, Centrum voor Wiskunde en Informatica, Amsterdam J. Lambek and P.J. Scott

[1986] An Introduction to Higher Order Categorical Logic, CUP Studies in Advanced Mathematics 7 S. Mac Lane

[1971] Categories for the Working Mathematician, Springer, 1971 J. Niño-Salcedo

[1981] On Continuous Posets and their Application, Ph.D. dissertation, Tulane University G.D. Plotkin

[1976] A Powerdomain Construction, SIAM J. Comp. 5 (1976) 452–487

[1978] The Category of Complete Partial Orders: A Tool for Making Meaning, Summer School on Foundations of Artificial Intelligence and Computer Science, Inst. di Sci. dell’Info., Univ. Pisa.

[1978] T^{ω} as a Universal Domain, J. Comp. Sys. Sci. 17 (1978) 209–236

[1982] , in Automata, Languages and Programming (Aarhus), ed. M. Nielsen and E.M. Schmidt,

Springer LNCS 140 G.D. Plotkin and M.B. Smyth [1978] Categorical Solution of Recursive Domain Equations, Dept. AI Research Report 60, Edin-

burgh

[1982] idem, Dept. Comp. Sci. Techn. Report 102, Edinburgh L.E. Sanchis

[1980] Reflexive Domains, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and

Formalism, ed. J.P. Seldin, J.R. Hindley, Academic Press D.S. Scott

[1972] Continuous Lattices, Toposes, Algebraic Geometry and Logic (Dalhousie 1971), ed. F.W. Lawvere, Springer LNM 274 (1972) 97–136

[1976] Data Types as Lattices, SIAM J. Comp. 5 (1976) 522–587 M.B. Smyth

[1983] The Largest Cartesian-Closed Category of Domains, Theor. Comp. Sci. 27 (1983) 109–119 J.E. Stoy

[1977] Denotational Semantics: the Scott-Strachey approach to Programming Languages, MIT Press,

Cambridge, Mass. P. Taylor

[1983] Applications of Continuous Lattices to Lambda Calculus and Denotational Semantics, Part III dissertation, University of Cambridge

[1985] Internal Completeness of Categories of Domains, Category Theory and Computer Programming (Guildford 1985), ed. D. Pitt et al., Springer LNCS 240 (1986) 449–465

[1986] Recursive Domains, Indexed Category Theory and Polymorphism, Ph.D. dissertation, University of Cambridge