An Algebraic Approach to Stable Domains

Paul Taylor

written 1988, published 1991

Abstract

Day [75] showed that the category of continuous lattices and maps which preserve directed joins and arbitrary meets is the category of algebras for a monad over Set, Sp or Pos, the free functor being the set of filters of open sets. Separately, Berry [78] constructed a cartesian closed category whose morphisms preserve directed joins and connected meets, whilst Diers [79] considered similar functors independently in a study of categories of models of disjunctive theories. Girard [85] built on Berry’s work to build a new and very lean model of polymorphism.

In this paper we bring these strands together, defining a monad based on filters of connected open sets and showing that its category of algebras has Berry’s (stable) morphisms and is cartesian closed. The objects have multijoins as in Diers’ work, and the slices are continuous lattices. The monad can only be defined for locally connected spaces, so via [Barr-Paré 80] there is a further (unexplained) connection with cartesian closure. Jung [87] has shown that the same objects (L-domains) also form a cartesian closed category with maps preserving only directed joins.

Berry’s proof of cartesian closure (using the trace factorisation, which also occurs in Diers’ work and is discussed in [Taylor 88]) and more direct proofs by Coquand [88] and Lamarche [88] use two additional hypotheses, strong finiteness and distributivity (of finite meets over finite joins). Our proof is the first to use neither of these, but it does use distributivity of codirected meets over directed joins, which [Taylor 88] shows not to be needed either. Lamarche has shown that evaluation does not preserve equalisers, so in the categorical context connected limits must be replaced by wide pullbacks. He has also found a generalised notion of neighbourhood system which unifies stable and continuous functions and generalises our ad hoc notion of Berry order between continuous functions.

Journal of Pure and Applied Algebra, 64 (1990) 171–203.

1 Preliminaries

1.1 Continuous Lattices and Posets

We shall need a number of standard results about continuous lattices (for which see [Gierz et al. 80] or [Johnstone 83] chapter VII). By a domain we shall simply mean a poset with directed joins (⋁ ; ): since we are not interested in fixed point properties, we have no need for ⊥.

Definition 1.1 Recall that x ≪ y (read: way below) in a domain if, whenever y ≤ ⋁ ; z_{i}, we already have x ≤ z_{i} for some i. A domain is continuous if every element is ≪-approximated, i.e.

∀x ∈ X.x = ⋁ ; ↓ ↓ x  where  ↓ ↓ x ≡ {x′ ∈ X : x′ ≪ x}

This says that amongst all the ideals with join x (of which ↓ x is the greatest), there is a least, namely ↓ ↓ x. Notice that it suffices that every principal lower set ↓ x be continuous.

Proposition 1.2 A complete lattice X is continuous iff it has the following directed distributivity property. Let {x_{jk} : j ∈ J, k ∈ K(j)} be a family of elements of X such that {x_{jk} : k ∈ K(j)} is directed for each j ∈ J. Let M = ∏_{j} K(j), i.e. the set of functions m : J → ⋃_{j∈J} K(j) with ∀j.m(j) ∈ K(j); this is directed in the componentwise order. Then

⋁ ; _{m∈M} ⋀_{j∈J} x_{j,m(j)} = ⋀_{j∈J} ⋁ ; _{k∈K(j)} x_{jk}

Proof Apply the adjoint functor theorem to the functor ⋁ ; : IdlX → X: this preserves meets iff distributivity holds, and the left adjoint (if it exists) is ↑ ↑. □

Definition 1.3 We shall usually consider domains to carry the Scott topology: U ⊂ X is open

if ⋁ ; x_{i} ∈ U ⇒ ∃i.x_{i} ∈ U.

The following results (like directed distributivity above) are standard: we include them here because they comprise most of what we need to know about continuous posets.

Exercise 1.4 In a continuous poset

(a) x ≪ y ⇒ x ≤ y and x′ ≤ x ≪ y ≤ y′ ⇒ x′ ≪ y′, and

(b) the sets ↑ ↑ x ≡ {y : x ≪ y} are open in the Scott topology and form a base for it. □

Lemma 1.5 The ≪ relation on a continuous poset has the interpolation property: if x ≪ z then x ≪ y ≪ z for some y. □

Exercise 1.6 A function between domains is Scott-continuous iff it preserves directed joins. □

Lemma 1.7 A Scott-continuous retract of a continuous poset is continuous. □

Definition 1.8 A homomorphism is a continuous function h : X → Y with a left adjoint c (with respect to the pointwise order); c itself is called a comparison. If c; h = id then the mono c is called an embedding and the epi h a projection.

Lemma 1.9

(a) h preserves all meets which exist.

(b) c preserves joins and the ≪ relation.

(c) Embeddings reflect ≪.

(d) The pullback of a projection against any continuous map is a projection. Proof

[a] Adjoint functor theorem.

[b] Let x_{0} ≪ x_{1} and cx_{1} ≤ y = ⋁ ; y_{i}. Then x_{1} ≤ h(⋁ ; y_{i}) = ⋁ ; hy_{i} by adjointness and continuity of h. But then x_{0} ≤ py_{i} for some i and so cx_{0} ≤ y_{i} as required.

[c] Let x_{0} ≤ x_{1} ≤ x′ = ⋁ ; x′_{i} with cx_{0} ≪ cx_{1}. Then for some i, cx_{0} ≤ cx′_{i} and so x_{0} = h(cx_{0}) ≤

h(cx′_{i}) = x′_{i}.

[d] The pullback of the projection p (with e ⊣ p) against the continuous map f is constructed in the same way in Set, Pos and Dom. We just have to check that the obvious thing, ⟨id, f ; e⟩, gives the left adjoint. □

1.2 L-Domains

We shall now introduce Jung’s [87] new category of L-domains. Definition 1.10 A connected meet in a poset P is the meet of over a diagram which is connected in the order-theoretic sense; thus pullbacks (meets of pairs with an upper bound) and codirected meets are connected but top and binary meets are not. In the categorical case, equalisers are also connected, although they are not simply connected as in [Taylor 87]. Definition 1.11 J ⊂ P is the multijoin of I ⊂ P if

(i) I ≤ J, i.e. ∀i ∈ I.∀j ∈ J.i ≤ j, and (ii) J is multiversal: if I ≤ p ∈ P, i.e. ∀i ∈ I.i ≤ p, then ∃!j ∈ J.j ≤ p. Note that j must be unique, so this is stronger than a set of minimal upper bounds as in Plotkin’s SFP-domains. For I = ∅, J is the set of least elements of the components of P; by binary multijoins we mean |I| = 2: J may have zero, one, finitely or infinitely many elements. Lemma 1.12 The following are equivalent for a poset P: (α) P has connected meets; (β) P has pullbacks and codirected meets; (γ) for all p ∈ P, ↓ p = {q ∈ P : q ≤ p} has arbitrary meets; (δ) for all p ∈ P, ↓ p is a complete lattice. (ϵ) P has multijoins.

Proof [α ⇔ β] Since any (connected) diagram is the filtered union of its finite (connected) subdiagrams,

any meet may be calculated as a codirected meet of finite meets. In posets finite connected diagrams reduce essentially to zig-zags, whose meets may be calculated using pullbacks. In categories we need to use equalisers too.

[β ⇔ γ] Pullbacks are binary meets below a fixed point, and codirected meets are eventually (and

w.l.o.g. always) so also. [γ ⇔ δ] Standard: the adjoint functor theorem for posets. [δ ⇔ ϵ] Likewise a poset is a complete lattice iff it has arbitrary joins, and having multijoins is the

same as having joins below any element. □ We are interested in connected meets, and wish to state directed distributivity for them. How-

ever it is difficult to see how this might be defined, other than that arbitrary meets distribute over directed joins below any element. In particular, directed distributivity says that meet, considered as a function of several (possibly infinitely many) arguments, is continuous in each of them separately (and hence jointly), but pullback is contravariant in one of its three arguments. Proposition 1.13 The following are equivalent for a domain X: (α) X has connected meets which distribute over directed joins. (β) for all x ∈ X, ↓ x is a continuous lattice; (γ) X has ≪-approximation, binary multijoins and ⊥ in each component; (δ) X is continuous and for all x ∈ X, ↓ x is a lattice.

Proof Observe that binary multijoins, ⊥ in each component and directed joins suffice to give all multijoins. □

Definition 1.14 Such a domain we call an L-domain, because it is obtained by patching together Lattices. Write LDom for the (2-)category consisting of L-domains, continuous maps (and the pointwise order). They already look like algebras for connected meets distributing over directed joins, so Scott-continuous maps are not their “natural” morphisms; we shall see this formally later.

Lemma 1.15 A (Scott-continuous) retract of an L-domain is an L-domain. Proof A retract of a continuous domain is continuous (1.1.7). For x ∈ X ◁ Y, ↓_{X} x ◁ ↓_{Y} i(x) and a retract of a lattice is a lattice. □

Note 1.16 Later we shall use the term stable domain to mean the same kind of object. However since we shall change the morphisms (and thereby obtain an exceedingly rich theory) we regard stable and L-domains as different things.

2 Connected Open Sets

2.1 Local Connectedness

Day’s [75] characterisation of continuous lattices (with arbitrary meets) uses filters of arbitrary open sets. We shall show that a similar result holds with connected instead. This requires us to have a good supply of connected open sets, and so we have to restrict to locally connected spaces. For a point of a space we have its filter of open neighbourhoods (open sets containing it); for a general space, there need be no connected open neighbourhood of a given point (and hence no filter): again we need local connectedness. Consequently this paper is not applicable to Stone spaces, which have hitherto been the heroes of categorical logic [Johnstone 83]. In particular we cannot replace the Scott topology on F_{dom} with the Lawson topology because in the important special case of algebraic lattices (or even coherent algebraic domains) it is a Stone space.

Definition 2.1 An open set is connected if it has no nontrivial expression as a disjoint union of open sets. This condition is also intended for an empty indexing set, so in particular a connected set is nonempty. We may write the condition on U as a scheme of axioms, one for each (“discrete”) set I, as follows:

⋀_{i≠j} [U_{i} ∩ U_{j} = ∅] ∧ [U = ⋃_{i} U_{i}]  ⊢ ⋁_{i} [U = U_{i}]

For I = 2 and I = ∅ we have the particular cases

U_{0} ∩ U_{1} = ∅ ∧ U = U_{0} ∪ U_{1}  ⊢ U = U_{0} ∨ U = U_{1}
U = ∅  ⊢ ⊥

Notice that it is provable from this that the disjunction on the right is disjoint (exactly one possibility holds), so connected open sets are an example of a disjunctive theory. We can make the corresponding definition for elements of a frame (locale), simply replacing ⋃, ∩ and ∅ by ⋁, ∧ and 0. Classically, the case for infinite I is redundant, but for an arbitrary base topos, even though “i ≠ j” requires I to be decidable, this is no longer true.

We shall generally (but not always) use U, V, etc. for connected open sets. The notation ∐ is used for a disjoint union.

Exercise 2.2 An open set which is connected in the order or (undirected) graph theoretic sense with respect to the specialisation order is connected in the topological sense. □

Definition 2.3 A topological space is locally connected if every open set is the union of the connected open sets which it contains.

Lemma 2.4 A space is locally connected iff every open set is uniquely expressible as a disjoint union of connected open sets (called its components). Proof [⇐] is obvious, so for [⇒] let X be locally connected and U ⊂ X open. Let C = {V connected open : V ⊂ U}, so by hypothesis ⋃ C = U. Let ∼ be the equivalence relation on C generated by the relation V_{1} ∩ V_{2} ≠ ∅. Since V_{1} ∩ V_{2} is by hypothesis a union of connected open sets, the latter is equivalent to ∃V ∈ C.V ⊂ V_{1} ∩ V_{2}.

For V ∈ C, let [V] = ⋃{V′ ∈ C : V ∼ V′}. This is open and contains V, so by local connectedness the union over V of these sets is U. If [V_{1}] ∩ [V_{2}] ≠ ∅ then V_{1} ∼ V′_{1} ∼ V′_{2} ∼ V_{2} for some V_{1} and V_{2}, so V_{1} ∼ V_{2} and [V_{1}] = [V_{2}]. Hence U is the disjoint union of the {[V] : V ∈ C}.

Let [V] = ∐_{i} W_{i} with W_{i} disjoint; then V = ∐_{i}(V ∩W_{i}) so V ⊂ W_{i_{0}} for some i_{0}. By induction on the definition of ∼ we show that V ∼ V′ ⇒ V′ ⊂ W_{i_{0}}. It suffices to do this for one step, so suppose V ∩ V′ ≠ ∅. By connectedness of V′ = ∐_{i}(V′ ∩ W_{i}), V′ = V′ ∩ W_{i_{1}} for some (unique) i_{1}. But ∅ ≠ V′ ∩ V ⊂ V′ ∩ W_{i_{0}}, so i_{1} = i_{0} and V′ ⊂ W_{i_{0}}. Hence [V] = W_{i_{0}} and is connected.

We have now expressed U as a disjoint union of connected open sets and it remains to show that this is unique. If U = ∐_{i} V_{i} = ∐_{j} W_{j} are two such decompositions, let T_{ij} = V_{i} ∩ W_{j}; then V_{i} = ∐_{j} T_{ij} so ∀i.∃!j.V_{i} = T_{ij}, say V_{i} = T_{i,j(i)}, and similarly W_{j} = T_{i(j),j}; hence i : J → I and j : I → J are mutually inverse bijections with V_{i} = W_{j(i)}. □

For an open set U of a locally connected space, K U denotes its set of components. As before we can define locally connected locales, and the lemma translates immediately.

Finally, a topological space is T_{0} if any two distinct points have some open set containing one but not the other. There is no need for such a definition with locales. In the case of domains the topological and order-theoretic or (undirected) graph-theoretic senses of connectedness coincide, so every domain is automatically T_{0} and locally connected.

Warning 2.5 For a continuous domain the basic open set ↑ ↑ x need not be connected. [For example take ℕ ∪ {∞} with the usual order: ↑ ↑ ∞ is empty; alternatively, in ℕ ∪ {∞, a, b} where a ≥ ∞ ≤ b it is disconnected.]

Definition 2.6 Write LCSp, LCLoc and Dom for the 2-categories of locally connected T_{0}- spaces, locally connected locales and (locally connected) domains. The morphisms in each case are (Scott) continuous maps (the opposite of frame homomorphisms). The 2-cells arise pointwise respectively from the specialisation order, inclusion of open sets and the given order relation. Pos denotes the 2-category of posets, monotone maps and the pointwise order.

2.2 Connected Open Filters

For X a domain or a locally connected T_{0}-space, write Ω(X) for its lattice of (Scott) open sets, which we consider to be a locale. For P a poset, write Υ(P) for the lattice of upper sets, which is also a locale (the Alexandroff topology). For A a locale, write C(A) for its subposet of connected elements. So C Ω(X) is the poset of connected open sets of a space or domain X and C Υ(P) is the poset of upper sets of P which are connected in the sense of (undirected) graphs. In both cases these are ordered by inclusion, but since they consist of upper sets, bigger sets have smaller elements.

For C any poset, let Filt(C) be the poset of filters (nonempty subsets ϕ ⊂ C with ∀c_{1}, c_{2} ∈ ϕ.∃c ∈ ϕ.c ≤ c_{1}, c_{2}), ordered by inclusion. Observe Filt(C) = Idl(C^{op}), so this is an algebraic domain and may be given the Scott topology, and continuous maps Filt(C) → X correspond bijectively to monotone maps C^{op} → |X|, where the latter denotes the poset of points of X with the specialisation order. Bigger filters contain smaller open sets (in the case where C = C(A)), which in turn contain bigger elements, so X and Filt C Ω(X) are now “the same way up”.

Definition 2.7 For a space X, let F_{sp}(X) = Filt C Ω(X) with the Scott topology; likewise for a domain D, let F_{dom}(D) = Filt C Ω(D). For a poset P, let F_{pos}(P) = (C Υ(P))^{op}. Finally, for a locale A, let F_{loc}(A) = Σ^{C(A)^{op}}.

Lemma 2.8 The following diagram commutes:

[figure: Pos; Idl; Dom; Scott; Sp; Ω; Loc]

[figure: Pos; F_{pos}; Idl; Dom; F_{dom}; Scott; Sp; F_{sp}; Ω; Loc; F_{loc}]

where additionally the composites along the top and bottom are Υ. Proof This is simply because F is defined as the composites of C : Loc → Pos with functors such as Ω, Idl and Scott. To check that the above formulae are correct, open sets of Filt C correspond (bijectively and preserving and reflecting order) to lower sets of C and hence to monotone functions C^{op} → Σ. □

In other words, the four Fs are essentially the same, and we shall use the subscripts to indicate whether we are thinking of F_{sp}(X) as a space, or F_{loc}(X) as a locale, or F_{pos}(X) as a poset or F_{dom}(X) as a poset with directed joins.

Lemma 2.9 The sets ⇈ U = {ϕ : U ∈ ϕ} ⊂ F_{sp}(X), for U ∈ C Ω(X), form a base for the topology on F(X), and ⇈ U ⊂ U iff ↑ U ∈ U, where ↑ U = {V ∈ C Ω(X) : U ⊂ V } ∈ F_{sp}(X). Proof The Scott topology on a space of filters is based by upper sets of compact filters, and a filter is compact iff it is the upper set of an element. □

In the localic case, we may recognise ⇈ : C(A) → F_{loc}(A) = Σ^{C(A)^{op}} as the Yoneda embedding.

Exercise 2.10 Let X be locally connected and ϕ ∈ Filt C Ω(X). Then ϕ is a semilattice, i.e. it has binary meets and a greatest element. □

Proposition 2.11

(a) F_{dom}(X) is an algebraic L-domain.

(b) F_{pos}(X) has ⊥ in each component and binary multijoins. Proof

[a] We already know that F_{dom}(X) is algebraic, so it remains to construct connected meets. Let ϕ_{(−)} : I → F_{dom}(X) be a connected diagram and ϕ = ⋂_{i} ϕ_{i}; we aim to show that ϕ ⊂ C Ω(X) is a filter. Each ϕ_{i} has some component of X as top element, and by connectedness of the diagram they must share the same component, which is therefore in the intersection and this is nonempty. Applying the same argument with X replaced by U ∩ V, where U, V ∈ ϕ, there is some connected open W ⊂ U, V in ϕ.

[b] The ⊥s correspond to the components of X and the multijoins to the component decompositions of intersections. □

2.3 The Functor

The idea of F(f) is simply the image:

F_{pos}(f)(U) = f[U] = {f(u) : u ∈ U}  2.11

recall that the image of a connected set is connected (we shall use the notation f[U] again). This does not extend immediately to spaces because the image of an open set need not be open. Let f : X → Y be continuous (in LCSp, LCLoc or Dom). In order to define a Scott-continuous function F(f) : F_{dom}(X) → F_{dom}(Y), it is necessary and sufficient to define a monotone function C Ω(X)^{op} → Filt C Ω(Y). Thus for U ∈ C Ω(X), let

F_{sp}(f)(↑ U) = {V ∈ C Ω(Y) : U ⊂ f^{−1}(V)}  2.11

This is obviously an upper set and anti-monotone in U, and defines

F_{sp}(f)(ϕ) = {V ∈ C Ω(Y) : ∃U ∈ ϕ.U ⊂ f^{−1}(V)}  2.11

Lemma 2.12 F(f)(↑ U) is a filter in C Ω(Y). Proof Again we need to use local connectedness. The component decomposition

Y = ∐_{a∈K(Y)} Y^{a}

yields a disjoint decomposition of X via f^{−1}, although the parts need not be connected (they are disjoint by the definition of a function). Hence U ⊂ f^{−1}Y^{a_{0}} for some (unique) a_{0}, and V = Y^{a_{0}} ∈ F(f)(↑ U) since it is connected. Similarly, if V is the component of V_{1} ∩ V_{2} which contains f[U], where V_{1}, V_{2} ∈ F(f)(↑ U), then V ∈ F(f)(↑ U). □

The localic form of F is given by

F_{loc}(f)^{∗}(⇈ V) = ∐ { ⇈ U : U ∈ K(f^{−1}(V))}  2.12
F_{loc}(f)^{∗}(V)  = ⋃ { ⇈ U : ∃V. ↑ V ∈ V ∧ U ⊂ f^{−1}(V)}  2.12
F_{loc}(f)_{∗}(U)  = ⋃ { ⇈ V : ∀U ∈ K(f^{−1}(V)). ⇈ U ⊂ U}  2.12

Lemma 2.13 F preserves identities and composition. Proof Clearly F(id)(↑ U) = ↑ U. Let f : X → Y and g : Y → Z be continuous and U ∈ C Ω(X). Then

F(g)(F(f)(↑ U)( = {W ∈ C Ω(Z) : ∃V ∈ C Ω(Y).U ⊂ f^{−1}(V) ∧ V ⊂ g^{−1}(W)}

We use the decomposition of g^{−1}(W) to reduce this to

{W ∈ C Ω(Z) : U ⊂ f^{−1}(g^{−1}(W))} = F(f ; g)(↑ U)  □

Lemma 2.14 F is faithful. Proof Let f, g : X ⇉ Y with F(f) = F(g). Then

∀U ∈ C Ω(X), V ∈ C Ω(Y).U ⊂ f^{−1}(V) ⟺ U ⊂ g^{−1}(V)

Using the decomposition of f^{−1}(V) and g^{−1}(V) (by local connectedness of X) we deduce that f^{−1}(V) = g^{−1}(V) for V connected. Using local connectedness of Y we extend this to all open V, and so the inverse image functions are equal. By T_{0}, f = g. □

In the same way we can prove

Exercise 2.15 F preserves and reflects natural transformations. □

F is not continuous on hom-sets with respect to this order. However we shall see in §4.1.2 that there is another order, the Berry order, which is also preserved and reflected by F(f). The functor is continuous on hom-sets with respect to this order.

2.4 Connected Open Neighbourhoods

The unit of Day’s monad defining continuous lattices was the filter of open neighbourhoods of a point. For x ∈ X ∈ LCSp or Dom, let

η_{X}(x) = {U ∈ C Ω(X) : x ∈ U}  2.15

The poset form is simply the up-closure:

η_{X}^{pos}(x) = ↑ x  2.15

Recall that the typical basic open set of F_{sp}(X) is

⇈ U = {ϕ ∈ F_{sp}(X) : U ∈ ϕ}  2.15

for U ∈ C Ω(X).

Lemma 2.16 η_{X}(x) is a filter and η_{X} : X → F_{sp}(X) is continuous. Proof The component of X containing x is the greatest element of η_{X}(x), and likewise U ∩ V has a component containing x. For continuity, η_{X}(x) ∈ ⇈ U ⟺ U ∈ η_{X}(x) ⟺ x ∈ U, so η_{X}^{−1}(⇈ U) = U. □

Lemma 2.17 Let A be a locally connected locale. Then

η^{∗} : U ↦ ⋃{u ∈ C(A) : ⇈ u ⊂ U}
η_{∗} : a ↦ ∐{⇈ u : u ∈ K(a)}

are the direct and inverse image parts of a continuous map η_{A} : A → F_{loc}(A) which coincides with η_{X} in the case A = Ω(X). Proof Observe that ⇈ U ∩ ⇈ V = {ϕ : U ∈ ϕ ∧ V ∈ ϕ}, which is the disjoint union of ⇈ W over the components W of U ∩ V. It follows that η^{∗} preserves disjoint unions (keeping them disjoint) and binary meets; since it is onto it also preserves ⊤ and ⊥. A general connected open set in F_{loc}(A) is a connected join of ⇈ u, and may be canonically so expressed by taking all possible u; it follows by monotonicity that η^{∗} is well-defined. Clearly η^{∗} has been defined to coincide with the spatial version. η_{∗} preserves disjoint unions, so η_{∗} ; η^{∗} = id_{A}. Conversely, ∐ ⇈ U_{i} ≤ ⇈ ∐ U_{i}, so η^{∗} ; η_{∗} ≤ id_{F_{loc}(A)} and η^{∗} ⊣ η_{∗}. □

Corollary 2.18 η^{∗} preserves connectedness and η_{∗} preserves disjoint unions; such a map we call locally dense. □

Exercise 2.19 η_{X} is an isomorphism iff X is an algebraic domain and every connected subset of X_{fp} has a least element.

Lemma 2.20 η : id → F is natural. Proof We have to show that the following diagram commutes for f : X → Y continuous:

[figure: F(X); F(f); F(Y); X; η_{X}; f; Y; η_{Y}]

In terms of elements (i.e. for LCSp), for x ∈ X,

F_{sp}(f)(η_{X}(x)) = {V ∈ C Ω(Y) : ∃U ∈ C Ω(X).x ∈ U ∧ U ⊂ f^{−1}(V)}

which reduces by local connectedness to η_{Y} (f(x)). For the localic version, we only have to show that

F_{loc}(f)^{−1}(⇈ V) = ∐ { ⇈ U : U ∈ K(f^{−1}(V))}

but ϕ ∈ F(X) is in either side iff f^{−1}(V) ∈ ϕ. □

2.5 Neighbourhoods of Sets

We can define the filter of connected open neighbourhoods of any connected set, not just of a singleton. (An arbitrary subset of a space is connected iff it is connected in the subspace topology.) For C ⊂ X connected, let

η_{X}⟨C⟩ = {U ∈ C Ω(X) : C ⊂ U}  2.20

this is nonempty because C lies in a component of X, and it is easy to show that it is a filter. In particular if U ∈ C Ω(X),

η_{X}⟨U⟩ = ↑ U  2.20

The poset form is equally simple,

η_{X}^{pos}⟨C⟩ = ↑[C]  2.20

A nucleus j on a locale A is connected if j(∐ U_{i}) = 1 ⊢ ∃!i.j(U_{i}) = 1; then

η_{A}⟨j⟩ = {U : j(U) = 1} ∈ F_{dom}(A)  2.20

(this defines a point, not an open set, of F(A)).

The relevance of this is that we defined

F_{sp}(f)(↑ U) = η_{Y} ⟨f[U]⟩  2.20

where f[C] = {f(x) : x ∈ C} is connected. This extends to arbitrary connected sets C:

F_{sp}(f)(η_{X}⟨C⟩) = η_{Y} ⟨f[C]⟩  2.20

We also have

η_{X}⟨C⟩ = ⋂{η_{X}(x) : x ∈ C} = ⋂ η_{X}[C]  2.20

Notice our careful use of special brackets: f[C] denotes the set of f(x) for x ∈ C, and η_{X}⟨C⟩ is an “overloading” of η where the argument is a connected set rather than an element.

2.6 Locally Connected Toposes

In this paper we shall work with component decompositions, but there is a slicker way of expressing local connectedness. Let U be any open set of a locally connected space X; we have written K(U) for its set of components. Because each component of a smaller set must lie in a unique component of a larger, this extends to a functor K : Ω(X) → Set. For any set Y, we write Δ(Y) for the discrete space with points Y. There is a continuous map U → Δ K(U) (which sends the whole of any component to its “name”), and this is universal in the sense that and map U → Δ(Y) to a discrete space factors as U → Δ K(U) → Δ(Y).

More generally, if U is a sheaf on X, it also splits into components, but now we can regard the discrete space as a constant sheaf on X. Then the universal property above becomes

K ⊣ Δ ⊣ Γ

where Γ(U) is the set of global sections of a sheaf, i.e. continuous maps from X splitting the local homeomorphism which displays U over X. K and Γ are functors E = Shv(X) → S = Set and Δ : S → E

In general, Δ : S → E is the inverse image functor of a geometric morphism, and preserves finite limits and arbitrary colimits. This means that we can do type-theoretic constructions in S involving finitary operators, equations, finite conjunctions, existential quantification and arbitrary disjunctions, i.e. geometric logic, and these will be preserved by Δ. In the case where E is (sheaves on) a locally connected space, Δ has a left adjoint (namely K), and consequently preserves infinitary limits, operations and conjunctions (and in fact also function-spaces and implications).

Actually, this is not quite right. Simply having a left adjoint K makes Δ preserve limits indexed by sets: if S is some (“more complex”) topos, its logic involves indexing over its own objects, which are not just discrete sets. What we need is that K be an S-indexed left adjoint. In this case we say that E is a locally connected topos over S, or that (Δ, Γ) : E → S is a locally connected geometric morphism.

Barr and Paré [80] have demonstrated in detail this link between local connectedness and preserving infinitary first-order predicate logic (including indexed products, as needed for infinitary operations). They call a topos E with this property molecular because its objects (“sheaves”) are disjoint unions (relative to S) of indecomposable components. These components are called molecules because they may be very complicated, unlike the atoms to which they reduce in the case where Δ is logical (preserves the subobject classifier, Ω): atoms have no nontrivial subobject. This phenomenon is discussed in Barr and Diaconescu [80], and is related to the versions of stable domain theory studied by Girard and Lamarche.

In another paper we shall show that the category of stable domains and stable functions is cartesian closed; it is very interesting to note that the precondition we need for constructing this category (viz. local connectedness) is itself closely linked with the same kind of structure. There must surely be a reason for this!

It would be nice to be able to extend the constructions of this paper to locally connected toposes. Unfortunately this is not possible in the obvious way, because C(E) ≅ K^{−1}(1) is a large category. The analogue of F_{loc}(E) would be the functor category [K^{−1}(1), Set], which is illegitimate and so not a (Grothendieck) topos. Even starting with (the topos of sheaves on) the Sierpiński space, we find ourselves freely adding pullbacks to the category • → •, whereas in the localic version we were merely filling in missing intersections. This irritating size problem could be solved either by requiring stable category-domains to have all maps mono and hence considering intersections (rather than wide pullbacks) and filtered colimits, or by asking for filtered colimits and cofiltered limits only of specified cardinalities.

3 The Algebraic Theory

3.1 Algebras for the Pointed Endofunctor

It turns out that we can define the algebras without the need for the multiplication part (μ) of the monad.

Definition 3.1 Given an (endo)functor F : C → C and a natural transformation (point) η : id → F, an algebra for (F, η) is an object X ∈ C together with a structure map ξ : F(X) → X such that the triangle

X \overline{η_{X}} F(X)

[figure: id]

X\begin{matrix}ξ \\  \end{matrix}

commutes. We can think of F(X) as “all polynomials in variables {x : x ∈ X} for the operations of the algebra”, η_{X}(x) as “the polynomial x” and ξ(p) for p ∈ F(X) as “p multiplied out in the structure (X, ξ)”.

We shall express the connected meet structure on a stable domain D in terms of a map ϵ_{D} : F(D) → D. To define such a continuous map, it is necessary and sufficient to give a monotone function C Ω(D)^{op} → D. This takes a connected open set to its (connected) meet. For general ϕ ∈ F_{dom}(D),

ϵ_{D}(ϕ) = ⋁ ; { ⋀ U : U ∈ ϕ}  3.1

Lemma 3.2 η_{D} ⊣ ϵ_{D} Proof For x ∈ D, ϕ ∈ F(D), we prove that

x ≤ ϵ_{D}ϕ ⟺ ∀y : x ∈ ↑ ↑ y.∃U ∈ ϕ.U ⊂ ↑ ↑ y ⟺ η_{D}(x) ⊂ ϕ

[a] Recall that x is ≪-approximated. Then for z ≪ x,

z ≪ ϵ_{D}ϕ ⟹ ∃U ∈ ϕ.z ≤ ⋀ U
⟺ ∃U ∈ ϕ.∀u ∈ U.z ≤ u

By ≪-interpolation (1.1.5) we can improve this to

y ≪ ϵ_{D}ϕ ⟹ ∃U ∈ ϕ.∀u ∈ U.y ≪ u
⟺ ∃U ∈ ϕ.U ⊂ ↑ ↑ y
⟹ y ≤ ϵ_{D}ϕ

[b] Let B be any basis for the topology on D; then the validity of

∀W ∈ B : x ∈ W.∃U ∈ ϕ.U ⊂ W

is independent of B. With B = {↑ ↑ y : y ∈ D} we recover the left hand side and with B = C Ω(D) the right. □

Lemma 3.3 η_{D} ; ϵ_{D} = 1_{D}. Proof For x ∈ D, clearly ϵ_{D}(η_{D}(x)) = ⋁ ; {⋀ U : x ∈ U} ≤ x. Let x′ ≪ x, so x ∈ U ⊂ ↑ ↑ x′ for some U ∈ C Ω(X); it suffices to show that x′ ≤ ϵ_{D}(η_{D}(x)). But x′ ≤ ⋀ U, which occurs in the join. □

Corollary 3.4 η_{D} is an embedding and ϵ_{D} a projection. □

Lemma 3.5 More generally, ϵ_{D}(η_{D}⟨C⟩) = ⋀ C for a connected set. Proof ϵ_{D} is a right adjoint and so preserves meets, and so

ϵ_{D}(η_{D}⟨C⟩) = ϵ_{D}( ⋀ η_{D}[C])  by (2.5.7)
= ⋀ ϵ_{D}[η_{D}[C]]  by (3.1.3)
= ⋀ C  by (3.1.4)

□

Lemma 3.6 (X, ξ) is an algebra for (F, η) iff X is an L-domain and ξ = ϵ_{X}.

Proof Firstly, X must be an L-domain, because η_{X} ; ξ = id_{X} makes X ◁ F(X), and L-domains are closed under Scott-continuous retracts (1.2.6). Hence ϵ_{X} exists and, since η_{X} ; ϵ_{X} = id, it is a structure map. On the other hand ϵ_{X} ≤ ξ since η_{X} ⊣ ϵ_{X}, so it only remains to prove ξ ≤ ϵ_{X}. It suffices to test this for compact filters, i.e. those of the form ↑ U = η_{X}⟨U⟩. But

ξ(η_{X}⟨U⟩) = ξ( ⋀ η_{X}[U])  by (2.5.7)
≤ ⋀ ξ[η_{X}[U]]  monotonicity
= ⋀ U  by (3.1.3)
= ϵ_{X}(η_{X}⟨U⟩)  by (3.1.6)

□

Exercise 3.7 Show that the algebras for the monad on Pos are posets with connected meets (1.2.3). The inclusion (by Idl) in the category of algebras for the other versions of the monad gives neither all algebraic stable domains nor all stable functions between them: characterise the ones it does give.

3.2 Homomorphisms for the Algebras

Definition 3.8 A homomorphism of (F, η)-algebras from (X, ξ) to (Y, υ) is a map f : X → Y in C which “preserves the structure” in the sense that

[figure: F(X); F(f); F(Y); X; ξ; f; Y; υ]

commutes; then we may “substitute and calculate” (clockwise) or “calculate and substitute” (anticlockwise). What are the homomorphisms of our algebras? Equivalently, since only ϵ is allowed as a structure map, with respect to what morphisms is ϵ natural? We must find out when this square commutes for ξ = ϵ_{D} and υ = ϵ_{E}.

Definition 3.9 Given a function f : X → Y in LDom, a left multiadjoint is a function k : Y → P(X) with the property that

y ≤ f(x) ⟺ ∃!x′ ∈ k(y).x′ ≤ x

Observe that f has a left adjoint iff (k exists and) each k(y) is a singleton.

Proposition 3.10 The following are equivalent for f : X → Y in LDom:

(α) f is an ϵ-homomorphism;

(β) f preserves all connected meets;

(γ) f preserves meets of connected open sets;

(δ) for all x ∈ X, the restriction of f to ↓ x → ↓ f(x) has a left adjoint;

(ϵ) f has a left multiadjoint; (ζ) for all y ∈ Y, f^{−1}(↑ y) is a disjoint union of principal upper sets; Proof

[α ⇒ β] Consider commutativity of the square at ϕ = η_{X}⟨C⟩. By (3.1.6), ϵ_{X}(η_{X}⟨C⟩) = ⋀ C, and by (2.5.7), F(f)(η_{X}⟨C⟩) = η_{Y} ⟨f[C]⟩. Substituting these, the clockwise route gives ⋀ f[C] and the anticlockwise route f( ⋀ C).

[β ⇒ γ] Trivial.

[γ ⇒ α] What we have is precisely commutativity of the square at compact filters. Since the functions are continuous and F(X) is algebraic, it holds everywhere.

[β ⇔ δ] Adjoint Functor Theorem.

[δ ⇔ ϵ] x′ ∈ k(y) is the value of this adjoint at y ∈ ↓ f(x).

[ϵ ⇔ ζ] f^{−1}(↑ y) = ∐{↑ x′ : x′ ∈ k(y)}. □

Definition 3.11 Such a map, which preserves directed joins and connected meets, is called stable. (Occasionally we use this word to refer specifically to the meet structure.) A stable domain is just an L-domain, but we use the different term to indicate its different morphisms. Write SDom for the category of stable domains and maps. There is an obvious forgetful functor U : SDom → LDom (we just forget that a function preserves connected meets), and we shall use this also for the composites with the other forgetful functors to LCSp, LCLoc and Dom.

Proposition 3.12 For any continuous f : X → Y, F(f) is a stable map. Proof The slick proof is to construct the multiadjoint. Essentially this takes V to the set of components of f^{−1}(V). More precisely, the compact filter ↑ V is mapped to the set k(↑ V) = {↑ U : U ∈ K(f^{−1}(V))}. Checking the multiadjunction for this,

↑ V ⊂ F(f)(ϕ) ⟺ V ∈ F(f)(ϕ)  F(f)(ϕ) is an upper set
⟺ ∃U ∈ ϕ.U ⊂ f^{−1}(V)  by (2.3.3)
⟺ ∃!U ∈ K(f^{−1}(V)).U ∈ ϕ  take U largest
⟺ ∃!ϕ′ ∈ k(↑ V).ϕ′ ⊂ ϕ  namely ϕ′ = ↑ U

The multiadjoint extends to arbitrary filters as follows:

k(ψ) = {ϕ′ : ∀U′ ∈ ϕ′.∃V ∈ ψ, U ∈ K(f^{−1}(V)).U ⊂ U′}  3.12

then ψ ⊂ F(f) ⟺ ∃!ϕ′ ∈ k(ψ).ϕ′ ⊂ ϕ, where

ϕ′ = {U′ ∈ ϕ : ∃V ∈ ψ, U ∈ K(f^{−1}(V)).U ⊂ U′}  3.12
□

Corollary 3.13 F = F ; U for a functor F : LCSp → SDom. □

Again we shall abuse notation and allow the argument of F to be a domain or locally connected space or locale.

3.3 Adjunction, Monad and Algebras

Proposition 3.14 F ⊣ U, with unit η and counit ϵ. Proof We showed one of the triangular identities in (3.1.4); for the other:

F(X) \overline{\begin{matrix}F(η_{X}) \\  \end{matrix}}F^{2}(X)

[figure: id]

F(X) \begin{matrix}ϵ_{F(X)} \\  \end{matrix}

By continuity we need only show this for ϕ = ↑ U = η_{X}⟨U⟩ with U ∈ C Ω(X). Then

ϵ_{F(X)}(F(η_{X})(η_{X}⟨U⟩)) = ϵ_{F(X)}(η_{F(X)}⟨η_{X}[U]⟩)  by (2.5.6)
= ⋀ η_{X}[U]  by (3.1.6)
= η_{X}⟨U⟩  by (2.5.7)

Where we have avoided discussing sets of sets of sets of sets by using the overloaded η and special brackets. □

It is instructive to see the adjoint correspondence.

f : X  → U(D)
F(X)  → U(D)
F(f) ; ϵ_{D} : F(X) → D

by

↑ U  ↦ ⋁ ; {⋀ V : U ⊂ f^{−1}(V)}  3.14
ϕ  ↦ ⋁ ; {⋀ V : ∃U ∈ ϕ.U ⊂ f^{−1}(V)}  3.14

and

s : F(X) → D
F(X)  → U(D)
η_{X} ; s : X  → U(D)

by

x  ↦ s(η_{X}(x))  3.14
⋃{U ∈ C Ω(X) : ⇈ U ⊂ s^{−1}(V)} ← V  3.14

Corollary 3.15 Any Scott-continuous map between L-domains factors as locally dense map (η — see 2.4.6) followed by a stable map. □

Definition 3.16 The connected open filter monad is that derived from the adjunction. The multiplication part of a monad says “remove the brackets” from polynomials of polynomials. We must have unit and associativity laws:

[figure: F; F(η); F^{2}; F^{3}; F(μ); F^{2}]

[figure: id]

[figure: F^{2}; η_{F}; μ; F; μ; F^{2}; μ_{F}; μ; F; μ]

which follow automatically if we put μ_{X} = ϵ_{F(X)}. In our case, we’ve just had a lucky escape from considering (sets of)^{5} sets! If we have an algebra for a monad, removing brackets from a polynomial of polynomials and calculating must be the same as calculating twice, so the diagram

[figure: F^{2}(X); F(ξ); F(X); F(X); μ_{X}; ξ; X; ξ]

must commute.

Theorem 3.17 SDom is the category of algebras for the monad; in other words the adjunction is monadic. Proof It only remains to check that (X, ϵ_{X}) satisfies the additional equation for an (F, η, μ)- algebra, i.e. that the above square commutes when we put ξ = ϵ_{X} and μ_{X} = ϵ_{F(X)}. This follows from the fact that ϵ_{X} : F(X) → X (horizontally) is a projection (3.1.5) and hence a stable map and ϵ : F → id (vertically) a natural transformation with respect to stable maps (3.2.3). □

3.4 Limits in SDom

Being able to express a category as a category of algebras gives us a good grasp on its structure, and in particular makes it easy to construct limits.

Theorem 3.18 Let U : A → C be the forgetful functor for a monad (it is called monadic or, ugh!, triplable). Then U creates limits, i.e. if d : I → A is any diagram such that d; U has a limit L in C (the limit of the “underlying objects”) then there is a unique structure map ξ : F(L) → L making (L, ξ) the limit in A with limiting cone that for C. U also creates regular monos (subalgebra inclusions). Proof See [Mac Lane 71], chapter III, [Manes 75] or [Barr and Wells 85], §3.4. □

Unfortunately our monad is not over Set, so it is not completely trivial. However we can do it indirectly. (The following results are exercises.)

Lemma 3.19 The underlying set functor Pos → Set is not monadic, but nevertheless creates limits. □

Proposition 3.20 Dom is the category of algebras for the monad (Idl, ↓, ⋃ ; ) on Pos. □

Corollary 3.21 SDom → Dom → Pos → Set creates limits. □

Exercise 3.22 Show that the forgetful functor SDom → Pos is also monadic. What is the relationship with the monad F_{pos}?

3.5 Injectivity

One of the earliest known properties of continuous lattices (with the Scott topology) was that they are exactly the injective T_{0}-spaces (or locales) with respect to subspace inclusions. Similarly one can show that boundedly-complete continuous posets are injective with respect to dense inclusions. What is the corresponding property for L-domains?

In terms of locales, i : X′ → X is a subspace inclusion iff i_{∗} ; i^{∗} = id, and then j = i^{∗} ; i_{∗} is a nucleus: it is inflationary, idempotent and preserves binary meets. Spatially,

i_{∗}(U) = int(U ∪ (X \ X′))

for U ⊂ X′ open. So i is dense iff i_{∗} (or j) preserves ⊥. We are looking for a stronger condition than density, and it turns out to be that i_{∗} (or j) preserves disjoint unions.

Definition 3.23 A continuous function f is locally dense if f_{∗} preserves disjoint unions.

Examples 3.24

(a) η_{X} : X → F(X) is locally dense and continuous (but not stable): 2.4.6;

(b) any stable map is locally dense iff it is a homomorphism. □

Lemma 3.25 The following are equivalent for a continuous map f : X → Y in LCLoc:

[α] f^{∗} preserves connectedness;

[β] f_{∗} preserves disjoint unions;

[γ] F(f) is a homomorphism. Proof

[α ⇔ β] Let V ∈ C Ω(Y) and U_{i} ∈ Ω(X) be disjoint. Then

∃!i.V ⊂ f_{∗}(U_{i}) ⟺ V ⊂ ∐_{i} f_{∗}(U_{i})  V connected
V ⊂ ∐_{i} f_{∗}(U_{i}) ⟺ V ⊂ f_{∗}( ∐_{i} U_{i})  [β]
V ⊂ f_{∗}( ∐_{i} U_{i}) ⟺ f^{∗}(V) ⊂ ∐_{i} U_{i}  f^{∗} ⊣ f_{∗}
f^{∗}(V) ⊂ ∐_{i} U_{i} ⟺ ∃!i.f^{∗}(V) ⊂ U_{i}  [α]
∃!i.f^{∗}(V) ⊂ U_{i} ⟺ ∃!i.V ⊂ f_{∗}(U_{i})  f^{∗} ⊣ f_{∗}

[α ⇔ γ] Comparing with the proof of Proposition 3.2.5, k(↑ V) is a singleton iff f^{∗} preserves connectedness. □

Proposition 3.26 I ∈ LCSp is injective with respect to locally dense subspace inclusions iff I ∈ LDom. Proof

[⇒] η_{I} : I → F(I) is such an inclusion, so id_{I} must extend to a postinverse and hence make I ◁ F(I).

[⇐] Let i : X ↪ Y be locally dense, so F(i) : F(X) → F(Y) has a left adjoint; but it is mono, so the adjoint is a postinverse c. For any f : X → I, let g = η_{Y} ; c; F(f) ; ϵ_{I}. Then

i; g = i; η_{Y} ; c; F(f) ; ϵ_{I}
= η_{X} ; F(i) ; c; F(f) ; ϵ_{I}  by naturality of η
= η_{X} ; F(f) ; ϵ_{I}  construction
= f ; η_{I} ; ϵ_{I}  by naturality of η
= f  by (3.1.4)

so g is the required extension of f. □

Lemma 3.27 In fact it is the greatest extension. For suppose f = i; h; then

h = h; η_{I} ; ϵ_{I} = η_{Y} ; F(h) ; ϵ_{I}  naturality of η
≤ η_{Y} ; c; F(i) ; F(h) ; ϵ_{I}  c ⊣ F(i)
= η_{Y} ; c; F(f) ; ϵ_{I} = g  □

Johnstone [83] uses the fact that exponentiation (by an exponentiable space) preserves injectivity to characterise the exponentiables spaces as those whose open set lattices are continuous (and in [81] the exponentiable toposes as those which are continuous categories; Hyland [81] gives the corresponding result for locales). Unfortunately I can’t see any similarly slick argument for Jung’s “exponentiability” result, since we now want X^{X} to be itself exponentiable.

Exercise 3.28 Show that the injectives for subalgebra inclusions in SDom are the continuous lattices. Hint: the four-point lattice has a two-point discrete subalgebra.

4 Cartesian Closure

4.1 The Berry Order

In this final section we shall exploit the characterisation we have given for stable domains in terms of operations and equations to prove that the category is cartesian closed. As usual, the main problem is to identify the exponential [A → B], whose points must correspond to stable maps from A to B since 1 generates in the category.

What must the order relation be? Suppose f ≤ g are two points of [A → B] enjoying the order relation between them, and a′ ≤ a two points of A. Then in the product [A → B] × A

⟨f, a′⟩ ≤ ⟨f, a⟩

⊼  ⊼

⟨g, a′⟩ ≤ ⟨g, a⟩

is a pullback, which must be preserved by the evaluation map ev : [A → B] × A → B since this is to be stable. Hence we make the following

Definition 4.1 Two stable functions f, g : A → B are said to be comparable in the Berry order, written f ⊑ B, if, for all a′ ≤ a ∈ A, f(a′) = f(a) ∧ g(a′).

This order relation is sparser than the pointwise order which we obtained from the monad (lemma 2.3.10), so what’s wrong with the monad? Simply that we took the wrong order relation between continuous functions in LCSp. Indeed,

Proposition 4.2 Let f, g : X ⇉ Y in LCSp with f ≤ g pointwise. Then the following are equivalent:

(α) F(f) ⊑ F(g)

(β) For all compact ϕ′ ≤ ϕ ∈ F(X) and ψ ∈ F(Y), if ψ ≤ F(f)(ϕ), F(g)(ϕ′) then ψ ≤ F(f)(ϕ′).

(γ) For all V ∈ C Ω(Y), K g^{−1}(V) ⊂ K f^{−1}(V). Proof [α ⇒ β] is trivial.

[β ⇒ α] Since F(Y) is algebraic, it suffices that ψ be compact; then ψ ≤ F(f)(ϕ_{0}), F(g)(ϕ′_{0}) for some compact ϕ_{0} ≤ ϕ and ϕ′_{0} ≤ ϕ′, and by directedness we may assume ϕ′_{0} ≤ ϕ_{0}.

[β ⇔ γ] (γ) means that if U′ ⊂ g^{−1}(V) and U ⊂ U′ ∩ f^{−1}(V) for some U, U′ ∈ C Ω(X) then U′ ⊂ f^{−1}(V). Put ϕ = ↑ U, ϕ′ = ↑ U′ and ψ = ↑ V; any compact ϕ′ ≤ ϕ ∈ F(X) and ψ ∈ F(Y) arise in this way. □

So we may take (γ) as the definition of the Berry order on continuous functions between locally connected spaces, and with this order the monad gives the Berry order on stable functions.

Returning to cartesian closure, in order that ev(f, a) be stable in f it is necessary (and sufficient) that directed joins and connected meets be constructed pointwise, and we devote the following two subsections to showing this. However it is essential that the systems of functions be directed (respectively connected) in the Berry order, because otherwise the result is a classic failure:

Example 4.3 Let A = ℕ ∪ {∞} with the usual order and B = Σ. Consider the (stable) functions f_{i} : A → B where f_{i}(n) = ⊤ if n ≥ i and ⊥ otherwise. Then (f_{i} : i ∈ ℕ) is a codirected system in the pointwise order, but

⋀_{i∈ℕ} f_{i}( ⋁ ; _{n∈ℕ} n) = ⊤ ≠ ⊥ = ⋁ ; _{n∈ℕ} ⋀_{i∈ℕ} f_{i}(n)

so ⋀ f_{i} is not continuous. By reversing the order we have a pointwise directed system of stable functions whose join is not stable. □

4.2 Directed Joins of Sections

Let f_{i} : A → B be a directed system (in the Berry order) of stable functions.

Lemma 4.4 f = λa. ⋁ ; _{i} f_{i}(a) is a stable, continuous function. Proof It is trivial to show that it is a continuous function. For stability of f, let (a_{j} : j ∈ J) be a connected system in A. By the stability of each f_{i} we have

l = ⋀_{j} f(a_{j}) = ⋀_{j} ⋁ ; _{i}f_{i}(a_{j}) ≥ ⋁ ; _{i}⋀_{j} f_{i}(a_{j}) = ⋁ ; _{i}f_{i}( ⋀_{j} a_{j}) = f( ⋀_{j} a_{j}) = r

and we must show the reverse inequality. Since B is a continuous poset, it suffices to show that if x ≪ l (which gives ∀j.∃i.x ≤ f_{i}(a_{j})) then x ≤ r. Choose j_{0} ∈ J arbitrarily, and suppose x ≤ f_{i_{0}}(a_{j_{0}}). By induction on the length of a zig-zag j_{0} ≤ j_{1} ≥ j_{2} ≤ ... ≥ j_{n} = j (using connectedness) to an arbitrary j ∈ J, we shall show that ∀j.x ≤ f_{i_{0}}(a_{j}). If j_{0} ≤ j_{1}, trivially x ≤ f_{i_{0}}(a_{j_{0}}) ≤ f_{i_{0}}(a_{j_{1}}). Suppose j_{0} ≥ j_{1}; we have x ≤ f_{i_{1}}(a_{j_{1}}) (with w.l.o.g. i_{0} ≤ i_{1}). So using f_{i_{0}} ⊑ f_{i_{1}} we have that

[figure: f_{i_{0}}(a_{j_{1}}); f_{i_{0}}(a_{j_{0}}); f_{i_{1}}(a_{j_{1}}); f_{i_{1}}(a_{j_{0}})]

is a pullback, whence x ≤ f_{i_{0}}(a_{j_{1}}). Now we have x ≤ ⋀_{j} f_{i_{0}}(a_{j}) ≤ r. □

Exercise 4.5 Explain how this proof avoids the counterexample (4.1.3).

Lemma 4.6 For each i, f_{i} ⊑ f. Proof For a ≤ b the rectangle

\begin{matrix}f_{i}(a) & \overline{} & f_{j}(a) & \overline{} & ⋁ ; f_{j}(a) \\ f_{i}(b) & & \overline{} & f_{j}(b) & & \overline{} & ⋁ ; f_{j}(b) & \end{matrix}

must be a pullback. As before, suppose y ≪ f_{i}(b), ⋁ ; f_{j}(a), so for some j (w.l.o.g. i ≤ j), y ≤ f_{i}(b), f_{j}(a). But f_{i} ⊑ f_{j}, so y ≤ f_{i}(a). □

Lemma 4.7 If ∀i.f_{i} ⊑ g, then f ⊑ g. Proof Again for a ≤ b the right-hand square

\begin{matrix}f_{i}(a) & \overline{} & ⋁ ; f_{i}(a) & \overline{} & g(a) \\ f_{i}(b) & & \overline{} & ⋁ ; f_{i}(b) & & \overline{} & g(b) & \end{matrix}

must be a pullback. Let y ≪ g(a), ⋁ ; f_{i}(b), so y ≤ g(a), f_{i}(b) for some i. But f_{i} ⊑ g, so y ≤ f_{i}(a) ≤

⋁ ; f_{i}(a). □

Proposition 4.8 The poset of functions with the Berry order has directed joins, and these are constructed pointwise. □

4.3 Connected Meets of Sections

Let f_{j} : A → B be a connected system (in the Berry order) of stable functions.

Lemma 4.9 f = λa. ⋀ f_{j}(a) is a stable, continuous function. Proof It is stable because connected meets commute with each other. The proof of continuity is essentially the same as that of stability of a directed join, but it is so remarkable that this argument works that it seems well worth repeating. Let (a_{i} : i ∈ I) be a directed system in A with a = ⋁ ; a_{i}; by continuity of each f_{j} and the definition of f we have

l = f( ⋁ ; _{i}a_{i}) = ⋀_{j} f_{j}( ⋁ ; _{i}a_{i}) = ⋀_{j} ⋁ ; _{i}f_{j}(a_{i}) ≥ ⋁ ; _{i}⋀_{j} f_{j}(a_{i}) = ⋁ ; _{i}f(a_{i}) = r

and we must show the reverse inequality. By continuity of B, it suffices to show that if x ≪ l (which gives ∀j∃i.x ≤ f_{j}(a_{i})) then x ≤ r. Choose j_{0} ∈ J arbitrarily, and suppose x ≤ f_{j_{0}}(a_{i_{0}}); by induction on the length of a zig-zag j_{0} ≤ j_{1} ≥ j_{2} ≤ ... ≥ j_{n} = j (using connectedness) to an arbitrary j ∈ J we shall show that ∀j.x ≤ f_{j}(a_{i_{0}}). If j_{0} ≤ j_{1}, trivially x ≤ f_{j_{0}}(a_{i_{0}}) ≤ f_{j_{1}}(a_{i_{0}}). Suppose j_{0} ≥ j_{1}; we have x ≤ f_{j_{1}}(a_{i_{1}}) (with w.l.o.g. i_{0} ≤ i_{1}). So using f_{j_{0}} ⊒ f_{j_{1}} we have

[figure: f_{j_{1}}(a_{i_{0}}); f_{j_{0}}(a_{i_{0}}); f_{j_{1}}(a_{i_{1}}); f_{j_{0}}(a_{i_{1}})]

is a pullback, whence x ≤ f_{j_{1}}(a_{i_{0}}). Now we have x ≤ ⋀_{j} f_{j}(a_{i_{0}}) ≤ r. □

Lemma 4.10 For each j, f ⊑ f_{j}. Proof We must show that the square

[figure: ⋀ f_{j}(a); f_{i}(a); ⋀ f_{j}(b); f_{i}(b)]

is a pullback for a ≤ b and some fixed i. Let y ≤ f_{i}(a), ⋀ f_{j}(b), so ∀j.y ≤ f_{j}(b). We have to show that y ≤ f_{j}(a) by induction on the length of a zig-zag from i to j. For a one-step path there are the two cases i ≤ j and i ≥ j; the first of these follows by f_{i} ⊑ f_{j}, whilst the second follows trivially since y ≤ f_{j}(a) ≤ f_{i}(a) in the pointwise order. For a longer path, j = i_{0} ≤ i_{1} ≥ i_{2} ≤ i_{3}... ≥ i_{n} = i, in the context of ∀i.y ≤ f_{i}(b) we use this to show that y ≤ f_{i_{k}}(a) ⇒ y ≤ f_{i_{k+1}}(a). □

Lemma 4.11 If ∀j.g ⊑ f_{j}, then also g ⊑ f. Proof Again for a ≤ b the left-hand square

[figure: g(a); ⋀ f_{i}(a); f_{i}(a); g(b); ⋀ f_{i}(b); f_{i}(b)]

must be a pullback. For any i, since g ⊑ f_{i}, the rectangle is a pullback, and by the right-hand square is too. □

Proposition 4.12 The poset of functions with the Berry order has connected meets, and these are constructed pointwise. □

4.4 Cartesian Closure

Proposition 4.13 The poset of stable functions with the Berry order is a stable domain, and evaluation at a chosen point is a stable function. Proof It only remains to show that arbitrary meets distribute over directed joins in each slice of the function-space. But meets and joins are calculated pointwise, so the result follows from distributivity in each slice of B. Stability of evaluation is the same as saying that directed joins and connected meets of functions are calculated pointwise. □

Lemma 4.14 ev : [A →^{s} X] × A → X is stable. Proof To show that it preserves filtered colimits we first observe that it is continuous in each argument separately. Then recall that separate and joint continuity are equivalent, because when we take the colimit twice over the same filtered diagram, we may replace it by the “diagonal”. The same argument applies to codirected meets.

The pullback diagram

[figure: ⟨f_{1}, a_{1}⟩; ⟨f_{2}, a_{2}⟩; ⟨f_{3}, a_{3}⟩; ⟨f_{4}, a_{4}⟩]

splits into pullbacks in [A →_{s} X] and in A. Then each square of

[figure: f_{1}(a_{1}); f_{1}(a_{3}); f_{3}(a_{3})]
f_{1} stable  f_{1} ⊑ f_{3}
[figure: f_{1}(a_{2}); f_{1}(a_{4}); f_{3}(a_{4})]
f_{1} ⊑ f_{2}  ev_{a_{4}} stable
[figure: f_{2}(a_{2}); f_{2}(a_{4}); f_{4}(a_{4})]

(which is part of a 4D cube) is a pullback. □ Theorem 4.15 SDom is cartesian closed. Proof The adjunctive correspondence (Currying) between f : A×B → C and g : A → [B →^{s} C] is completely standard. The counit is ev, which we have already shown to be stable, whilst the unit is a ↦ (b ↦ ⟨a, b⟩). For fixed a, b ↦ ⟨a, b⟩ preserves directed joins and connected meets (but not ⊤ or ⊥), and (since they are constructed pointwise for functions) so does a ↦ (b ↦ ⟨a, b⟩). Naturality and the triangular identities are standard and trivial. □

5 Bibliography

M. Barr and R. Diaconescu

[80] Atomic Toposes, Jou. Pure Appl. Alg. 17 (1980) 1–24 M. Barr and R. Paré

[80] Molecular Toposes, Jou. Pure Appl. Alg. 17 (1980) 127–132 M. Barr and C. Wells

[85] Toposes, Triples and Theories, Springer Gr. d. Math. Wis. 278 (1985)

G. Berry

[78] Stable Models of Typed λ-Calculi, ICALP, Springer LNCS 62 (1978) 72–89 Th. Coquand

[87] Categories of Embeddings, Logic in Computer Science (Edinburgh, 1988), Computer Science

Press, 256–263 Th. Coquand, C.A. Gunter and G. Winskel

[86] DI-domains as a Model of Polymorphism, University of Cambridge Computer Laboratory technical report 107 (1986)

[87] Domain-Theoretic Models of Polymorphism, ibid. 116 (87)

A. Day

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

[77] Catégories Localisables, thèse de doctorat d’état, Paris VI, 1977 [79] Familles Universelles de Morphismes, Ann. Soc. Sci. Bruxelles (1979) 93–111

[79] Some spectra relative to functors, Jou. Pure Appl. Alg. 22 (1979) 57–74

[80] Catégories Localement Multiprésenatables, Archive der Mathematik 34 (1980) 344–356 [80] Catégories Multialgébriques, Archiv der Mathematik 34 (1980) 193–209

[80] Quelques constructions de catégories localement multiprésentables, Ann. Sc. Math. Québec IV/2 (1980) 79–101

[80] Multimonads and Multimonadic Categories, Jou. Pure Appl. Alg. 17 (1980) 153–170

[81] Complétions monadiques de quelques catégories sans produit, Rendiconti di Matematica VII/1 (1981) 559–669

[84] Une construction universelle des spectres, topologies spectrales et faisceaux structuraux,

Comm. Alg., (1984) 2141–2183 P. Gabriel and F. Ulmer

[71] Lokal Präsentierbare Kategorien, Springer LNM 221 (1971)

G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove and D.S. Scott [80] A Compendium of Continuous Lattices, Springer

J.-Y. Girard

[81] Π_{2}^{1}-logic, Part I: Dilators, Ann. Math. Logic, 21 (1981) 75–219

[84] Normal Functors, Power Series and λ-calculus, Ann. P.&A. Logic, 1986

[85] The System F of Variable Types, Fifteen Years Later, Theor. Comp. Sci. 45 (1985) 159–192 J.-Y. Girard, translated and with appendices by Y.G.A. Lafont and P. Taylor

[89] Proofs and Types, CUP Cambridge Tracts in Theoretical Computer Science 7 J.M.E. Hyland

[81] Function Spaces in the Category of Locales, in Continuous Lattices, ed. Banaschewski &

Hoffman P.T. Johnstone

[80] A Syntactic Approach to Diers’ Localizable Categories, Sheaves and Logic (Durham, 1977), ed. M.P. Fourman, C.J. Mulvey and D.S. Scott, Springer LNM 753 (1980) 466

[82] A topos-theorist looks at dilators, manuscript, 22pp

[83] Stone Spaces, CUP St. Adv. Maths. 3 P.T. Johnstone and A. Joyal

[82] Continuous Categories and Exponentiable Toposes, J. Pure Appl. Alg. 25 (82) 255-296 A. Joyal

[87] Foncteurs analytiques et espèces de structures, Combinatoire énumérative (Montréal, 1986),

Springer L.N. Mathematics 1234 (1987) 126–159 A. Jung [87] Cartesian Closed Categories of Algebraic CPOs, Fach. Math. Techn. Hochsch. Darmstadt,

preprint 1110 (1987)

[88] Cartesian Closed Categories of Domains, doctoral dissertation, Fach. Math. Techn. Hochsch.

Darmstadt A. Kock

[73] Monads for which Structures are Adjoints to Units, in Springer LNM 420 F. Lamarche

[87] A Model for Coquand’s Theory of Constructions, Comptes Rendues Roy. Soc. Canada, 1987

[87] A Simple Model for the Theory of Constructions, Categories in Computer Science and Logic, AMS Contemporary Mathematics, 1987

[88] Modelling Polymorphism with Categories, Ph.D. dissertation, McGill Univ.

[89] Generalised spaces, seminar S. Mac Lane

[71] Categories for the Working Mathematician, Springer Graduate Texts in Maths. E.G. Manes

[75] Algebraic Theories, Springer Grad. Texts. Maths. 26 J. Meseguer

[83] Order Completion Monads, Alg. Univ. 16 (1983) 63–82 D.S. Scott see also G. Gierz

[72] Lattice Theory, Data Types and Semantics, Formal Semantics of Programming Languages, 1970 , 65-106, Prentice-Hall,

[76] Data Types as Lattices, SIAM J. Comp. 5 (1976) 522-587,

[82] Domains for Denotational Semantics, Automata, Languages & Programming, ed. M. Nielsen

& E.M. Schmidt, Springer LNCS 140 (1982) 577–613 P. Taylor

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

[87] Homomorphisms, Bilimits and Saturated Domains, manuscript, 30pp

[88] The Trace Factorisation and Cartesian Closure for Stable Categories, manuscript, 70pp [89] Quantitative Domains, Groupoids and Linear Logic, Category Theory and Computer Science

(Manchester, September 1989), Springer LNCS, to appear.