Non-Artin Gluing in Recursion Theory and Lifting in Abstract Stone Duality

Paul Taylor

August 5, 2003

Abstract Stone duality is a radical reformulation of general topology, in which the topology on a space X is not considered as a set carrying an infinitary lattice structure, but as another space that’s the exponential Σ^{X} in the category. In this way it restricts attention to recursive unions, in place of arbitrary ones, and thereby provides a natural formulation of computably based locally compact spaces [E], into which traditional arguments involving open and compact spaces nevertheless lift very easily.

As ASD axiomatises spaces and continuous functions directly, arguments involving points and non-continuous functions cannot be imported directly into it. In fact, “underlying sets” may be added as a further axiom, with the result that the theory is equivalent to the standard one for locally compact locales over an elementary topos [G], but the recursive character is thereby lost.

The difficulty over arbitrary unions cannot be defined away by substituting recursive ones. They are used very heavily in traditional topology, often in the guise of the right adjoints to which they give rise, the most familiar being the interior of a subspace. The categorically more sophisticated treatment in locale theory shows this very clearly, and introduces further ideas that depend on such right adjoints, notably the nucleus of a subspace. We cannot, therefore, expect every topological idea to survive the unification with recursion theory.

ASD does not completely deprive us of tools besides the continuous functions X → Y themselves, as we may also use continuous functions between the spaces Σ^{Y} and Σ^{X}. In the traditional formulation, these spaces carry the Scott topology, and “Scott-continuous” functions are those between the infinitary lattices that preserve directed joins. All frame homomorphisms are Scottcontinuous, but Scott-continuous functions in general need not preserve finite meets and joins. Continuous functions between the spaces that the frames represent in locale theory correspond, of course, to frame homomorphisms in the opposite direction.

The general plan for translating a theorem of topology into abstract Stone duality is therefore to massage the localic formulation in such a way that only Scott-continuous functions between frames are used. In particular, direct image maps (f_{∗}) and Heyting implications have to be eliminated. Except, that is, in the special situations in which they are Scott continuous, such as !_{∗} for ! : K → 1, where K is compact. It is in this fashion that we formulate a particular technique in topology in Sections 1–5 of this paper, before adapting it to abstract Stone duality. Thus you can appreciate the topological ideas without first studying the abstract setting.

Our argument then “factors through” the interpretation of abstract Stone duality, in the sense that, for example, what we say concretely about Scott continuous functions between frames is replaced by use of abstract morphisms Σ^{Y} → Σ^{X} in the category axiomatised by ASD. You have to read the paper twice: once wearing localic spectacles, then again in terms of abstract Stone duality; on each reading, certain parts may be transparent (i.e. vacuous) and others opaque (not soundly defined). The strictly recursion-theoretic point of view is confined to Example 4.3.

The particular topological question considered in this paper is the recovery of a space Γ from an open subspace U and its complementary closed subspace C. (We also need some information about how they fit together.) Michael Artin showed that the frame of open subsets of Γ may be expressed as a comma square that involves the frames corresponding to U and C and a functor linking them. Artin actually studied this problem for Grothendieck toposes [AGV64, Exposé IV, §9.5] [Joh77, Theorem 4.27], but we shall only consider locales, first recalling Artin’s construction in this rather simpler setting.

Our interest is specifically in the classifier for partial maps with open domain of definition. This is found as a special case of gluing, written Γ = U_{⊥} and called the lift of U, where C = {⊥} is a closed point. Clearly the lift is an important step in the development of domain theory and the semantics of programming languages, and Section 8 uses it to construct the search or minimalisation operation for general recursion in domain theory.

The humble partial map classifier is also related to many other universal properties [DT87, especially Section 4]. In particular, X_{⊥} is the partial product of the object X along the morphism ⊤ : 1 → Σ. In topology, partial products were introduced by Boris Pasynkov [Pas65] and studied further by Susan Niefield [Nie82]. They are in turn a special case of dependent products, which capture the universal quantifier categorically. Conversely, the considerably more complicated construction of dependent products can actually be reduced to partial products [Tay99, §9.4]. Future work will construct (some) partial products in abstract Stone duality from the partial map classifier. In view of the difficulty in constructing this one special case, such simplifications are extremely valuable.

Unfortunately, in Section 4 we find that Artin’s cosy relationship between open and closed subspaces in traditional topology fails entirely when we consider a recursively enumerable (semidecidable) set of numbers and its complement. The Artin gluing construction is therefore an example of something in point-set topology that depends on the use of functions that are not Scott-continuous, and does not survive the desired unification with recursion theory. So Artin is rather a “straw man” in this paper — he is set up only to be knocked down. The role of the counterexample in the construction of the partial map classifier is to anticipate a “why can’t you just” question.

Nevertheless, by further massaging of the argument, we find that the partial map classifier may still be constructed as a special case of Artin gluing. The proof is of course lattice-theoretic, and ASD requires topologies to be distributive lattices just as traditional formulations do, but we find that the crux is not distributivity but the modular law.

We said in the opening paragraph that arguments involving open and compact subspaces may be lifted very easily into ASD. In fact, morphisms Σ^{Y} → Σ^{X} that preserve the finitary lattice operations can be shown to be of the form Σ^{f} for f : X → Y. Using this result, it is actually quite easy to show that the Artin gluing construction yields the partial map classifier.

However, these results depend on the axiom of ASD, known as the Scott principle, that provides as much infinitary structure as is appropriate to recursion theory, and thereby fixed points in domain theory. On the other hand, [C] showed that many important notions in topology (such as compact Hausdorff spaces) already have a natural formulation and familiar properties without this axiom. The weaker theory is precisely lattice dual between open and closed phenomena, but this duality is broken by the extra axiom — as of course it must be in order to recover the standard theory completely.

There is another reason^{1} for developing the partial map classifier or lift without the Scott principle. Other authors in synthetic domain theory have discussed alternatives to this axiom that involve an isomorphism between the initial algebra and final coalgebra for the lift functor, (−)_{⊥}. For them, this functor plays the fundamental role that Σ^{(−)} has in ASD. In order to make use of their alternative fixed point axioms, we have to construct the lift without using the Scott principle.

As we cannot therefore characterise inverse image maps Σ^{f} as lattice homomorphisms Σ^{Y} → Σ^{X}, we have to deal explicitly with Eilenberg–Moore homomorphisms for the monad on which ASD is based. The fully massaged topological argument leaves us at the end of Section 5 with an order-isomorphism, namely the one that states the modular law. In the traditional or localic setting, every order-isomorphism is a frame isomorphism. In ASD, we still have to show that it is an Eilenberg–Moore isomorphism, which we do in Section 7.

1There is of course the mathematician’s favorite answer to the question of why they want to investigate something, namely “because it’s there”. In particular, the construction in this paper was developed when only the results of [C] and [B, Section 7] were available, so Eilenberg–Moore algebras and their homomorphisms had to be manipulated directedly. However, those who like to use this quotation from George Mallory, who had been asked why he wanted to climb Everest, should bear in mind that he died there a year later.

1 Gluing as a comma square

We shall use the letters Γ, U, C, ... in the same roles throughout the paper.

Notation 1.1 Let U, C ⊂ Γ be complementary open and closed subspaces, as indicated by the different hooks on the arrows. Then there are the following adjunctions of monotone functions amongst the frames A, S and G of open subsets of U, C and Γ respectively.

U  A

Γ^{\begin{aligned}i & open \\ &  \end{aligned}∩}  G [figure: ∃_{i} ≡ i_{!}]⊣ i^{∗}[figure] ⊣ \begin{matrix}i_{∗} \\  \end{matrix} . . . . . . . . . . . . . . . .

C^{c closed_{⊔} }  S [figure: c_{!}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .]⊣ [figure: c^{∗}] ⊣ \begin{matrix}∀_{c} ≡ c_{∗} \\  \end{matrix}

For open subsets W ⊂ Γ, T ⊂ U and D ⊂ C, the inverse image maps i^{∗} and c^{∗} and their adjoints act as follows:

i^{∗}(W) = W ∩ U ⊂ U
c^{∗}(W) = W ∩ C ⊂ C
∃_{i}(T) = T ⊂ Γ
i_{∗}(T) = (U ⇒ T) = int(T ∪ C) ⊂ Γ
∀_{c}(D) = D ∪ U ⊂ Γ.

We write i_{∗} as a dotted line because this monotone function between frames is not in general Scott-continuous (Examples 1.5). On the other hand, although it may lack its right adjoint, i^{∗} does preserve all joins, both finite and (where they exist) directed.

Remark 1.2 The other map that we have drawn dotted (c_{!}) does not exist in the general open– closed situation, whatever our axiomatisation of topology. In this paper, however, we shall specifically be interested in the case where the closed subset C is {⊥}, ⊥ being the least point of the lift or scone (Sierpiński cone) Γ = U_{⊥}. In this case the continuous map c : {⊥} → Γ is left adjoint (in the ordered category of spaces, continuous maps and the specialisation order) to the terminal projection !_{Γ} : Γ → 1. In terms of frames, c_{!} = !_{Γ}^{∗} is the left adjoint of c^{∗} = !_{∗}. Hence

!_{Γ}^{∗}c^{∗}W = Γ | (⊥ ∈ W), which, classically, is \{ \begin{matrix}Γ & if ⊥ ∈ W \\ ∅ & otherwise. \end{matrix}

All three maps between S and G are Scott-continuous.

Lemma 1.3 (a,b) Disjointness of U and C is expressed by the equations

c^{∗}∃_{i}(T) = c^{∗}∃_{i}(U) = ∅ ⊂ C  or, equivalently,  i^{∗}∀_{c}(∅) = i^{∗}∀_{c}(D) = U

for open T ⊂ U and D ⊂ C, whilst (c,d) the fact that they cover Γ is stated for open W ⊂ Γ by

∃_{i}i^{∗}(W) ∪ c_{!}c^{∗}(W) = W  or  i_{∗}i^{∗}(W) ∩ ∀_{c}c^{∗}(W) = W.  □

Notation 1.4 It is natural to try to use some combination of the six morphisms in Notation 1.1 to recover the frame G from A and S. In view of the disjointness characterisation in the Lemma, we are obliged to make use of one or other of the dotted maps, so we write

ℓ ≡ i^{∗} · c_{!} : S → A  and  r ≡ c^{∗} · i_{∗} : A → S  so ℓ ⊣ r.

Examples 1.5

(a) For the disjoint union U + C of two clopen subsets, ℓ(D) = ∅ ⊂ U, r(T) = C and G ≅ S × A.

(b) Let Γ = [0, 1] be the real unit interval, which is a compact Hausdorff space, and let U be (0, 1], which is an open subset that is not closed. Put T_{n} = (2^{−n}, 1]. Then i_{∗} and r do not preserve the directed union ⋃ T_{n} = (0, 1], since 0 ∈ i_{∗}U.

(c) For the scone or lift (Γ = U_{⊥}), ℓ = i^{∗} ·!_{Γ}^{∗} = !_{U}^{∗} by Remark 1.2, which is the inverse image map corresponding to the terminal projection !_{U} : U → 1, so it is a homomorphism. Hence ℓ has a right adjoint r that is Scott-continuous iff U is a compact space [C, Definition 7.7].

(d) Likewise, for the inverted scone Γ = C^{⊤} (drop, dunk or dip, maybe), r = !_{C}^{∗} is the homomorphism corresponding to the terminal projection !_{C} : C → 1, and has a left adjoint ℓ iff C is an open or overt space [loc. cit.].

(e) In the sheaf analogue of U_{⊥}, which is known as the Freyd cover, ℓ is the functor that assigns constant sheaves on U to “sets” s ∈ S, and its right adjoint r is the global sections functor.

(f) In the analogous situation in recursion theory, however, the set U ⊂ ℕ of Gödel numbers of programs that terminate and its complement C are not glued together in anything like this way (Example 4.3).

What we learn from these examples is that, although r is always available in the traditional axiomatisation of point-set topology, it need not be Scott-continuous, so it cannot be used in abstract Stone duality. On the other hand, ℓ may sometimes exist, in which case it is necessarily continuous, and can be used in the construction instead of r. However, there are analogous situations in recursion theory where neither ℓ nor r nor anything similar is available.

Remark 1.6 Artin showed that the frame G is given by the comma square S ↓ r on the right:

[figure: ℓ ↓ A; i^{∗}; A; S ↓ r; i^{∗}; A; S; c^{∗}; ℓ; A; id; ↗; S; c^{∗}; id; S; r; ↗]

but, when ℓ ⊣ r both exist, this is isomorphic to the comma square on the left, because

ℓ ↓ A ≡ {(s, a) | ℓ(s) ≤ a} = {(s, a) | s ≤ r(a)} ≡ S ↓ r.

There are many accounts of the gluing construction using r : A → S, (for example [Tay99, § 7.7], where it is written U : A → S), so for the sake of variety we shall give it in terms of ℓ. This is the version that we require for the scone or lift, which will turn out to classify partial maps with open domain of definition. On the other hand, the inverted scone classifies partial maps defined on closed subsets, and this is constructed from r.

We have just given the “set-theoretic” formulae for the comma squares, which are good enough for the purposes of this paper, but the categorical definition is contained in the proof of the next result.

Proposition 1.7 G is the comma square ℓ ↓ A in the ordered category of frames and Scottcontinuous functions. Proof Let S ^{s} Δ ^{a} A be functions such that i^{∗} · c_{!} · s ≤ a. I claim that g = ∃_{i} · a ∨ c_{!} · s : Δ → G is the unique function with c^{∗} · g = s and i^{∗} · g = a.

Δ  \overline{a}

[figure: G; i^{∗}; g; .; .; .; .; .; .; .; .; .; .; .; .; .; A]

[figure: s; S; c^{∗}; ℓ = i^{∗} · c_{!}; A; id; ↗]

This follows from Lemma 1.3 and the fact that i^{∗} and c^{∗} preserve binary joins, which are constructed componentwise in ℓ ↓ A as ℓ itself preserves binary joins. □

Remark 1.8 If a and s preserve ⊤ then so does g (by Lemma 1.3(c)); if a and s preserve Iindexed joins then so does g, and if a ⊣ a_{∗} and s ⊣ s_{∗} then g ⊣ g_{∗} = a_{∗} · i^{∗} ∧ s_{∗} · c^{∗}. To see that g preserves ∧ so long as a and s do, observe that ℓ ↓ A is a subframe of S × A, with ∧ constructed componentwise. □

Conversely, any such ℓ : S → A yields an open–closed pair.

Proposition 1.9 Let ℓ : A → S be a function between frames that preserves ⊥ and ∨. Then there are adjoint monotone functions between frames as shown,

\begin{matrix}ℓ ↓ A & [figure: ∃_{i}; ⊥; i^{∗}] & A \\ S & [figure: c_{!}]⊣ [figure: c^{∗}] ⊣ \begin{matrix}∀_{c} \\ \end{matrix} & \overline{ℓ} & A & {id \atop } & ↗ \end{matrix}

where

(a) π_{1} = i^{∗} and π_{0} = c^{∗} are frame homomorphisms,

(b) i^{∗} preserves whatever joins ℓ does,

(c) if ℓ has a right adjoint, ℓ ⊣ r, then so does i^{∗}, namely i_{∗}(a) = (r(a), a),

(d) i^{∗} has a left adjoint, ∃_{i}(a) = (⊥, a), satisfying the Frobenius law,

∃_{i}(a ∧ i^{∗}g) = (∃_{i}a) ∧ g,

so i is an open inclusion [C, Proposition 3.11],

(e) c^{∗} has a right adjoint, ∀_{c}(s) = (s, ⊤), which is Scott -continuous (even if ℓ isn’t) and satisfies the lattice dual of the Frobenius law, so c is a closed inclusion [C, Corollary 5.6],

(f) c^{∗} has a left adjoint c_{!}(s) = (s, ℓ(s)),

(g) ℓ = i^{∗} · c_{!}, so c_{!} is a homomorphism iff ℓ is. Hence the inclusions ∃_{i} and ∀_{c} make A ≅ (G ↓ u) and S ≅ (u ↓ G) as open and closed sublocales respectively, where u = (⊥, ⊤) ∈ ℓ ↓ A. □

2 The partial map classifier

Our main interest in this paper is to show that the lift (X_{⊥}), which we construct as an example of Artin gluing, also has a quite different universal property in the category of spaces.

Definition 2.1 The open inclusion i : X ^{⊂}  X̃ is the partial map classifier for X if, given

any partial map Γ ⇀ X (defined by p : U → X, where i : U ^{⊂} Γ is another open inclusion), there is a unique map f : Γ → X̃ such that the square is a pullback.

[figure: U; p; X; Γ; j; ∩; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; f; X̃; i; ∩]

In terms of frames, f^{∗} must be a homomorphism such that j^{∗} · f^{∗} = p^{∗} · i^{∗} and f^{∗}X = U.

Remark 2.2 In the case where X is a singleton, {⊤}, this reduces to the diagram that defines the open-subobject classifier, Σ [C, Definition 2.2]. This has the same definition as the subobject classifier Ω in an elementary topos, apart from the restriction from all to just open subsets. In topology, Σ is the Sierpiński space, ⊤ is its open point and ⊥ the closed one.

Although the analogy between Ω in set theory and Σ in topology is often exploited in abstract Stone duality, it does not extend to the construction of the corresponding notions of partial map classifier. We have embarked on a study of the gluing construction, which only provides X̃ in topology, not intuitionistic set theory, where we must use the rather uninformative formula

X̃ = {ξ ∈ Ω^{X} | ∀x, y ∈ X. x ∈ ξ ∧ y ∈ ξ ⇒ x = y}.

So the construction works only under some special condition, which we can easily identify by considering the case X = 1, where A = Σ^{X} = Σ and the gluing construction gives

Σ^{X_{⊥}} = G = ℓ ↓ Σ = {(s, a) ∈ Σ × Σ | s ≤ a} ≡ Σ^{≤},

with ℓ = r = id_{Σ}. The necessary condition is therefore

Definition 2.3 The Phoa principle is that Σ^{Σ} ⊂ Σ^{2} is the order relation that arises from the lattice structure on Σ. Symbolically, this means that

F : Σ^{Σ}, σ : Σ ⊢ F σ = F ⊥ ∨ σ ∧ F ⊤,

whilst topologically it says that the two elements ⊤, ⊥ : Σ of the Sierpiński space classify open and closed subspaces respectively.

This principle emerged from Wesley Phoa’s Ph.D. thesis about synthetic domain theory [Pho90a, Pho90b]. It is a trivial fact about the classical Sierpiński space, but is proved for intuitionistic locale theory and stated as an axiom of abstract Stone duality in [C, Section 5]. The link relation, x ⊑_{L} y, which says that there is a “path” from x to y (measured by Σ, rather than by the real unit interval as in homotopy theory), was also introduced by Phoa. It is indiscriminate for (classical or intuitionistic) sets, but agrees with the specialisation order for topology, where all functions Σ → Σ are monotone.

Lemma 2.4 The map b : 1 → X̃ that classifies 1 _{⊃} ∅ X is the least element of X̃. Proof Consider the dotted map h : X̃ × Σ → X̃, where the squares and parallelograms in the diagram are pullbacks. The upper composite X̃ → X̃ is id, so h(ξ, ⊤) = ξ ∈ X̃, whilst the lower one 1 → X̃ is b, so h(ξ, ⊥) = b.

X
[figure: X; id; id; X; 1]
∅  \overline{}
X̃
[figure: X̃ × Σ; i × ⊤; ∩; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; h; (id, ⊤); X̃; i; ∩; Σ; ⊤]
[figure: 1; (b, ⊥)]

This means (by definition) that b ⊑_{L} ξ in the link order. Then the composites

[figure: ΣX̃; h^{∗}; Σ^{X̃×Σ} ≅ (ΣX̃)^{Σ} ≅ (ΣX̃)^{≤}; ev_{⊤}; ev_{⊥}; ΣX̃]

are !_{Γ}^{∗} · b^{∗} ≤ id_{H}. But b^{∗} ·!_{Γ}^{∗} = id_{Σ} anyway, so !_{Γ}^{∗} ⊣ b^{∗}. □

As we need to prove a Theorem (5.1) to show that the gluing construction X_{⊥} satisfies the universal property of the partial map classifier X̃, we use the term lift to mean this special case of the Artin construction.

Definition 2.5 The lift of a space X is the space X_{⊥} whose topology is obtained by gluing:

\begin{matrix}X_{⊥} & i _{⊃} & X & H = Σ^{X_{⊥}} = ℓ ↓ A & \overline{i^{∗}} & A \\ \{⊥\} & \begin{matrix}b_{⊔} & \\ ⊣ \begin{matrix}!_{X_{⊥}} \\ \end{matrix} \end{matrix} & Σ & \begin{aligned}b_{!} = !^{∗} & \\ & ⊣ \begin{matrix}b^{∗} \\ \end{matrix} \end{aligned} & \overline{ℓ = !_{X}^{∗}} & A = Σ^{X} & {id \atop } & ↗ \end{matrix}

H = Σ^{Γ} = {(s, a) ∈ Σ × A | ℓ(s) ≤ a}, where ℓ = !_{X}^{∗} in Proposition 1.9.

Remark 2.6 In classical topology [AAB80], X_{⊥} is the union of the open subset X and the closed point {⊥}. The pullback condition in Definition 2.1 of the partial map classifier says that f : Γ → X_{⊥} takes the value ⊥ throughout the closed subset C that is complementary to the open subset U ⊂ Γ on which p : U → X is defined.

This situation is, therefore, an example of the effect on morphisms of the gluing of complementary open and closed subspaces (gluing as a functor). As such, it is given in terms of frames by the mediator f^{∗} between comma squares, as shown in the diagram on the right below.

[figure: X_{⊥}; i  _{⊃}; X; Σ^{X_{⊥}}; i^{∗}; Σ^{X}]

[figure: Σ^{Γ}; j^{∗}; f^{∗}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{U}; p^{∗}]
[figure: Γ; j _{⊃}; f; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; U; p]
Σ^{\{⊥\}} \begin{aligned}b^{∗} \\ &  \end{aligned}

[figure: {⊥}; b_{⊔}; !_{C}; C; c_{⊔}; Σ^{C}; c^{∗}; id; !_{C}^{∗}; Σ^{C}; c^{∗} · j_{∗}; ↗]

Remark 2.7 Although the topology on X_{⊥} itself is constructed using a comma square, the square whose universal property we are using to show that X_{⊥} classifies partial maps is the one for the arbitrary open–closed pair U, C ⊂ Γ. The ℓ and r versions of Proposition 1.7 then offer the formulae

∃_{i}p^{∗}a ∨ c_{!}!_{C}^{∗}s  and  j_{∗}p^{∗}a ∧ ∀_{c}!_{C}^{∗}s

respectively for the mediator f^{∗}(s, a). However, c_{!} need not be defined, and j_{∗} need not be Scottcontinuous.

In fact, f^{∗}(s, a) = !_{Γ}^{∗} ∨ ∃_{j}p^{∗}a. This makes the parallelogram on the left commute because

c^{∗}f^{∗}(s, a) = c^{∗}!_{Γ}^{∗}s ∨ c^{∗}∃_{j}p^{∗}a = !_{C}^{∗}s ∨ ⊥ = !_{C}^{∗}b^{∗}(s, a)

by Lemma 1.3(a) and Proposition 1.9(a). The one at the top commutes because

j^{∗}f^{∗}(s, a) = j^{∗}!_{Γ}^{∗}s ∨ j^{∗}∃_{j}p^{∗}a = !_{U}^{∗}s ∨ p^{∗}a = p^{∗}a

since j^{∗} · ∃_{j} = id as j is mono, and

!_{U}^{∗}s = p^{∗}!_{X}^{∗}s = p^{∗}ℓs ≤ p^{∗}a

by the construction in Definition 2.5.

For locales, the same argument as in Remark 1.8, namely that Σ^{Γ} is a subframe of Σ^{U} × Σ^{C}, shows that (whatever the formula for it actually is) the mediator is unique and is a frame homomorphism. In view of the counterexample in Section 4, Σ^{Γ} is not given by a comma square, so we must find a different way to justify this formula for the total extension f of the partial map p.

3 Modularity and distributivity

The modular law was first identified by Richard Dedekind in 1900, though, as he used the term Dualgruppe for lattice, this work went unrecognised until Øystein Ore co-edited his Gesammelte mathematische Werke in 1932. It plays a very important role in the structure theory of certain kinds of algebra, notably submodules (hence the name) and normal subgroups, where it is known by names such as the “nth isomorphism theorem” (1 ≤ n ≤ 4) and Zassenhaus’s butterfly lemma. In linear algebra it is directly connected with the notion of dimension, whilst in group theory it shows how to decompose any (finite) group into an invariant collection of simple groups.

How is this relevant to gluing?

Remark 3.1 Recall from Lemma 1.3 that any open subset W ⊂ Γ may be recovered as

W = V ∪ Z = I ∩ J

where

V = c_{!}c^{∗}(W)  Z = ∃_{i}i^{∗}(W)  I = i_{∗}i^{∗}(W)  J = ∀_{c}c^{∗}(W)

(are open subsets of Γ but) are used to represent open subsets of U or C. (As usual, c_{!} and V only exist for the lift, where C = {⊥}.) These subsets form a sublattice of G (the topology on Γ) as shown:

int(W ∪ C) ∪ U = I ∪ U

I = i_{∗}i^{∗}W = int(C ∪ W)^{− ∪ U }  W ∪ U = ∀_{c}c^{∗}W = U ∪ V = J

[figure: W; − ∪ U; U; − ∩ U]

[figure: V = !^{∗}c^{∗}W = Γ | (⊥ ∈ W); U ∩ W = ∃_{i}i^{∗}W = I ∩ U = Z; − ∪ U; − ∩ U]

U ∩ V = U | (⊥ ∈ W)^{− ∩ U }

Remark 3.2 The open subspace W is uniquely determined by either of the equations

W ∩ U = Z  or  W ∪ U = J,

together with the requirement that it be sandwiched amongst I, J, V and Z. We concentrate on the equation Z = W ∩ U, of which the solution is W = Z ∪ V. □

This last observation, which will be the basis of our proof in Section 5, is just the modular law:

Definition 3.3 In any lattice we have an adjunction

E = \{(u, v, z) | (u ∧ v ≤ z ≤ u\} [figure: [v ∨ z/w]; ⊥; \underline{[u ∧ w/z]}] \{(u, v, w) | v ≤ w ≤ u ∨ v\} = F.

The lattice is modular if this is an isomorphism.

Examples 3.4 This characterisation says that the lattice contains no configuration of the type (a), i.e. in any such situation, in fact w_{1} = w_{2}:

\begin{aligned}& u ∨ w_{1} \\ w_{2} \\ & & u \\ w_{1} \\ (a) & u ∧ w_{2} \end{aligned}  \begin{matrix}u ∨ w_{1} = u ∨ w_{2} \\ w_{1} & u & w_{2} \\ u ∧ w_{1} = u ∧ w_{2} & (b) \end{matrix}

The distributive law implies the modular law, but the modular lattice (b) is not distributive.

Remark 3.5 There are many ways of stating modularity as an equation, but I have always got lost when trying to use them: you only have to look at the proof of the Jordan–Hölder theorem in any random book on group theory to see how much care is needed to obtain a clear argument that involves this law. It seems to be much easier just to evaluate the expressions that you want to study in the free modular lattice on three variables {t, u, v}, which appeared in Dedekind’s original paper. (Really it would be nicer in 3D, as it has three wings and two cubes.)

⊤
m = (t ∨ u) ∧ (t ∨ v) ∧ (u ∨ v)
t ∨ u ∨ v ∘
∘  ∘  ∘ t ∨ v
∘  ∘  ∘ (t ∨ v) ∧ (u ∨ v)
∘  m ∘  ∘  ∘ (t ∧ u) ∨ v
u ∘  u′ ∘  t′ ∘  ∘ v′ ∘ t  ∘ v
u ∧ (t ∨ v) ∘  n ∘  ∘  ∘ (t ∨ u) ∧ v
u ∧ ((t ∧ u) ∨ v) ∘  ∘  ∘ (t ∧ v) ∨ (u ∧ v)
t ∧ u ∘  ∘  ∘
∘ t ∧ u ∧ v
u′ = (u ∧ (t ∨ v)) ∨ (t ∧ v)  n = (t ∧ u) ∨ (t ∧ v) ∨ (u ∧ v)
⊥

Notice Example 3.4(b) in the middle, whilst the other bold edges express the distributive law itself. Any lattice image of the diagram that collapses one of these twelve edges kills the others too, leaving the free distributive lattice on {t, u, v}.

Remark 3.6 We have just provided a visual and intuitionistic proof that a lattice is distributive iff it contains neither of Examples 3.4. □

In this work we are just flirting with the mysterious beauty of the modular law, as we make no suggestion that general topology can be formulated using anything less than distributivity. The reason for doing things in terms of modularity is that the isomorphism in Definition 3.3 is the substance of our construction in Sections 5 and 7.

Back to gluing. There doesn’t seem to be any formula to recover W from Z and J without using either I or V, but we shall use an argument similar to Remark 3.1 to prove Theorem 5.1 for the lift. We can, however, show that W is at least uniquely determined by Z and J, so Σ^{Γ} is a subalgebra of Σ^{U} × Σ^{C}.

Lemma 3.7 Let U, C ⊂ Γ be the complementary open and closed subspaces, and W_{1}, W_{2} ⊂ Γ open subsets that have the same restrictions to U and C, i.e.

Z = W_{1} ∩ U = W_{2} ∩ U  and  J = W_{1} ∪ U = W_{2} ∪ U.

Then W_{1} = W_{2}. More generally, if ϕ, ψ : Γ ⇉ Σ^{Δ} agree on both U and C then they are equal. Proof This says that if Example 3.4(b) occurs as in Σ^{Γ} or Σ^{Δ×Γ} then W_{1} = W_{2}, which is equivalent to the distributive law by Remark 3.6. □

Definition 3.8 We say that e : X → Y is Σ-epi if Σ^{e} : Σ^{Y} → Σ^{X} is mono.

So e satisfies the usual definition of epi (indeed internally),

[figure: X; e; Y; f; g; Σ^{Δ}]

that e; f = e; g ⇒ f = g, so long as the common target of the pair is a power of Σ. A continuous map of spaces is Σ-epi iff it hits enough points of Y to distinguish its open subsets, whilst a continuous map of locales is Σ-epi iff it is an epimorphism.

Theorem 3.9 {⊥, ⊤} → Σ is stably Σ-epi.

[figure: {⊥, ⊤}; Σ; C + U; Γ; ϕ; ψ; Σ^{Δ}]

Proof As Σ is a distributive lattice, the coproduct 1+1 is stable under pullback [C, Theorem 9.2], and yields the diagram shown. Then U + C → Γ is Σ-epi by Lemma 3.7. □

Corollary 3.10 Let f : Γ → Θ be any continuous map such that the images of U and C both lie within the subspace M ⊂ Θ. Then the image of Γ is also contained in M.

By a “subspace” of a locale here we mean that m : M ↣ Θ is regular mono, and for abstract Stone duality m is to be extremal mono [Tay91], although when we use this result in the next section m is split mono.

[figure: M; U + C; {⊤, ⊥}; Θ; Γ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ]

Proof This is just an application of the orthogonality of epis and regular monos of locales, or of Σ-epis and extremal monos in abstract Stone duality. □

4 The failure of Artin gluing

We saw in Section 1 that open and closed subspaces may be glued by a comma square involving either ℓ or r, but that we could not rely on having one or other of these functions available in all circumstances: r may exist in topology as a monotone but not Scott-continuous function between frames, whilst ℓ is only defined in special cases.

In this section we show that, in classical recursion theory, recursively enumerable subsets are not glued to their complements by means of any comma square whatever. Then we adapt the argument to discrete and Hausdorff spaces in abstract Stone duality.

As Artin gluing is a well known technique in standard topology and locale theory, the “failure” that we are about to discuss does not apply to that situation, and the “counterexample” is actually a well known result. It says that, if a space is “discrete” in the sense that all singletons are open, then so too are all closed subspaces.

However, as in any “algebraic” or “type-theoretic” (re)axiomatisation of a mathematical topic, we are simultaneously interested in two models in particular: the classical one from which we are drawing our intuition, and the free or term model of the new axioms. The Halting Set is a feature of the term model, and is constructed in [F]. The real unit interval, which we shall use later in this section, is defined using the new axioms (and therefore in any model) in [E].

Definition 4.1 Writing Σ^{Γ} for the lattice of open or recursively enumerable subsets of any object Γ, we shall call a complementary open/closed (or RE/coRE) pair U, C of Γ Artinian if there is some comma square,

[figure: G = Σ^{Γ}; i^{∗}; A = Σ^{U}; S = Σ^{C}; c^{∗}; ℓ; Θ; r; ↗]

in which ℓ and r are any continuous (or computable) functions whatever — not necessarily those defined in Notation 1.4.

Remark 4.2 For the sake of directness, and in the absence of any suitable well known category for recursion theory, we introduce the idea of the counterexample in an entirely classical way. The letters U, C, T, D ⊂ ℕ below denote ordinary sets of numbers, and Σ^{ℕ} is merely an unusual name for the lattice of all recursively enumerable subsets of ℕ. There is no abstract categorical setting, and Σ^{ℕ} is not an exponential; indeed, there is no object to call Σ. Also, the object Θ in the Definition that ought to be variable will just be taken to be Σ^{ℕ} too.

Σ^{ℕ} is a “topology” on ℕ only in the sense of the intuitive analogy between open and recursively enumerable subsets, since this lattice does not have arbitrary joins. This intuition is good enough for our purpose: we only need ℕ, and not Σ^{ℕ}, to get the counterexample. The Rice–Shapiro and Myhill–Shepherdson theorems impress themselves as topological ideas more forcefully on anyone familiar with the Scott topology for a lattice such as Σ^{ℕ} (but who still considers ℕ to be topologically discrete in the strongest sense), but we don’t need anything so complicated to make our point.

Just as we normally do with open subsets of subspaces in point-set topology (Notation 1.1), we represent a recursively enumerable set T ⊂ U ⊂ ℕ of terminating programs by T = T ∩ U itself, and an RE set D ⊂ C ⊂ ℕ of non-terminating programs as D ∪ U. As before, A and S respectively denote the lattices of all such subsets.

The example illustrates yet again that something may be defined pointwise in recursion theory but not as a computable function.

Example 4.3 Consider ℕ as the set of Gödel numbers for programs that run without input. Let U ^{⊂} ℕ be the recursively enumerable subset consisting of terminating programs, and C ^{⊏} ℕ its complement.

I claim that, if U and C were Artinian, we would have a solution to the Halting Problem. Proof Suppose that there are computable functions ℓ and r such that G, A, S and Θ form a comma square:

U, C ⊂ ℕ  \overline{T_{n} = ∅}

[figure: G = Σ^{ℕ}; i^{∗} ≡ − ∩ U; W_{n}; .; .; .; .; .; .; .; .; .; .; .; .; .; A]

[figure: D_{n} = {n} ∪ U; S; c^{∗} ≡ − ∪ U; ℓ; Θ = Σ^{ℕ}; r; ↗]

We shall test the alleged comma square with maps T_{(−)} : ℕ → A and D_{(−)} : ℕ → S as shown in the diagram that assign recursively enumerable subsets of the two subspaces to each program n ∈ ℕ in a computable way. For the “triangles” to commute we need

i^{∗}W_{n} = W_{n} ∩ U = T_{n} ∩ U = ∅  and  c^{∗}W_{n} = W_{n} ∪ U = D_{n} ∪ U = {n} ∪ U.

• But if n ∈ C, so n ∉ U, the second equation gives n ∈ W_{n}, whilst

• if n ∈ U, it gives W_{n} ⊂ U, but W_{n} ∩ U = ∅ by the first equation, so n ∉ W_{n} = ∅. Hence W_{(−)} : U → G by n ↦ ∅ and W_{(−)} : C → G by n ↦ {n} are well defined, but if the mediator W_{(−)} : ℕ → G were represented by a program, the diagonal evaluation “ n ∈ W_{n}” would solve the Halting Problem.

We still have to show that the maps ℕ ⇉ Θ do in fact form a lax square that needs a mediator to the supposed comma square. Note that we already have a diagram of computable functions: the only question is whether the inequality holds between them.

Since mediators U → G and C → G do exist, the squares U ⇉ Θ and C ⇉ Θ are indeed lax. This means that ℓD_{n} ≤ θ (where θ ≡ r∅ ∈ Θ) for all n ∈ U, and also for all n ∈ C. Hence it is true for all n ∈ ℕ, so ℕ ⇉ Θ satisfy the inequality, as it is defined pointwise. □

Now we return to using Σ^{ℕ} etc. as exponentials, according to the usual formalism of abstract Stone duality, which can be interpreted in the categories of locally compact sober spaces or locales. We shall adapt the foregoing argument to show that the only Artinian pairs of subspaces in either a discrete or a Hausdorff space are the decidable ones. On the face of it, the last paragraph of the proof makes blatant use of excluded middle, but Corollary 3.10 will provide the justification at this point in the argument for locales or abstract Stone duality.

Definition 4.4 [C, Section 6]

(a) A space Γ is discrete if the diagonal Γ ↪ Γ×Γ is open. The classifying map (=_{Γ}) : Γ×Γ → Σ is called equality and its exponential transpose {−} : Γ → Σ^{Γ} the singleton, so each {n} ⊂ Γ is an open subspace.

(b) Similarly, Γ is Hausdorff if the diagonal is closed, with classifier (≠_{Γ}) : Γ × Γ → Σ. Then there is a continuous function n ↦ Γ \ {n}, making each {n} is closed, so Γ is T_{1}.

Theorem 4.5 If U, C is an Artinian open–closed pair in a discrete space Γ then C is also open.

U, C ⊂ Γ  \overline{T_{n} = ∅}

[figure: G = Σ^{Γ}; i^{∗} ≡ − ∩ U; W_{(−)}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; A]

[figure: D_{n} = {n} ∪ U; S; c^{∗} ≡ − ∪ U; ℓ; Θ; r; ↗]

Proof Define T_{(−)} : Γ → A and D_{(−)} : Γ → S as before. We need to solve the equations

i^{∗}W_{n} = W_{n} ∩ U = T_{n} ∩ U = ∅  and  c^{∗}W_{n} = W_{n} ∪ U = D_{n} ∪ U = {n} ∪ U.

The open space R = {n | n ∈ W_{n}}, i.e. the one classified by Γ ^{⟨id,W ⟩} Γ × Σ^{Γ} ^{ev} Σ, satisfies R ∩ U = ∅ by the first equation and R ∪ U = Γ by the second, so it is the complement of U. But C ∩ U = ∅ and C ∪ U = Γ too, so C = R [C, Proposition 9.5].

Again we have the question of whether the maps Γ ⇉ Θ form a lax square, that is, whether ℓ · D_{(−)} ≤ θ, where θ ≡ r∅ ∈ Θ. We know that the restrictions to U and C have this property, and the inclusion M = (Θ ↓ θ) ↣ Θ is split by (−) ∧ θ, so Corollary 3.10 applies. □

The Theorem is, of course, well known in traditional point-set topology: if every singleton is open then so is every subset.^{2} The difference is that, in the term model of abstract Stone duality, the topology Σ^{ℕ} on ℕ consists of the recursively enumerable subsets, and in particular the Halting Set is open but not closed.

2In the classical notion of discreteness, any subset is the union of its singletons, but this union is indexed by (the underlying set of) the subspace itself, and adjoining “underlying sets” to the recursive axiomatisation of abstract Stone duality yields standard locale theory [G].

Abstract Stone duality (as far as it has been developed in [A, B, C] and here) has a tight lattice duality between open and closed concepts, so the Theorem is also true of Hausdorff spaces. This result even tells us something new about spaces or locales as traditionally axiomatised: whilst Artin gluing works for ℝ, for example, it necessarily involves maps between frames that are not Scott continuous (Example 1.5(b)).

Theorem 4.6 If U, C is an Artinian open–closed pair in a Hausdorff space Γ then C is also open. Proof The contravariance argument in Example 4.3 and Theorem 4.5 relies on having n ∈ D_{n} and n ∉ T_{n} for all n, so when {n} is closed rather than open, we put D_{n} = Γ and T_{n} = U \ {n}. Then in the final paragraph we require ℓΓ ≡ θ ≤ rT_{n}, so for Corollary 3.10 we use M = (θ ↓ Θ) ↣ Θ, which is split by (−) ∨ θ. □

Remark 4.7 One might suppose that the failure of Artin gluing is simply a lack of ingenuity: that we just need cleverer formulae than Artin’s to characterise when open subsets D ⊂ C and T ⊂ U glue together, and to name their union. However, closer inspection of the arguments that we have used shows that

gluability of (D, T) ∈ Σ^{C} × Σ^{U} is not equationally characterised

because m : Σ^{Γ} ↣ Σ^{C} × Σ^{U} is not the equaliser of any pair of maps into a power of Σ. Proof If it were such an equaliser, m would be extremal mono, whilst U + C ↠ Γ is Σ-epi, but (T_{(−)}, D_{(−)}) : Γ → Σ^{C} ×Σ^{U} in Theorems 4.5 and 4.6 do not factor through Σ^{Γ} as in Corollary 3.10.

□

For locally compact Hausdorff locales, this result says that m is not the equaliser of any pair of Scott-continuous maps between frames. You may also like to translate the statement into recursion theory yourself, but it becomes rather long-winded without an adequate categorical setting.

5 The partial map classifier again

Despite the failure of the Artin comma square, Definition 2.5 (the lift) still gives the partial map classifier (Definition 2.1), and we have the formula for the mediator in Remark 2.7:

f^{∗}(s, a) = !_{Γ}^{∗}s ∨ ∃_{j}p^{∗}a.

The following proof settles the question for locales or traditionally defined spaces. It can also be adapted to abstract Stone duality, but does not complete the proof in that situation, as it only provides a lattice homomorphism f^{∗}. Therefore we still have to show that this is an Eilenberg– Moore homomorphism, as we shall do in Section 7. In fact, the additional argument is redundant in the presence of the Scott continuity axiom, as then every lattice homomorphism is an Eilenberg– Moore homomorphism [E].

Theorem 5.1 Lifting provides the partial map classifier. Proof According to Definition 2.1, we are given the maps p, i and j that are shown in bold in the following diagram, and have to find a map f, shown dashed, that makes the square a pullback. Moreover, f has to be unique. We shall capture f by defining Y ≡ f^{∗}W for any open subset W ⊂ X_{⊥}.

\begin{matrix}Z = p^{∗}i^{∗}W = \\ j^{∗}f^{∗}W = Y ∩ U \end{matrix}  \overline{}i^{∗}W = W ∩ X

[figure: U; p; ⊂; ∩; X; !_{X}; ⊂; {⊤}; A = Σ^{X}]

[figure: Y = f^{∗}W; \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}; .....; .; .; .; .; .; .; .; .; .; .; .; W]

Γ^{\begin{aligned}j \\ &  \end{aligned}∩}  ^{f}^{⊂...............}  X_{⊥}^{\begin{matrix}i \\  \end{matrix}∩}  \overline{}\frac{⊂}{}Σ^{∩}  Σ^{X_{⊥}} \begin{matrix}\begin{aligned}∃_{i} \\ &  \end{aligned} &  \\ ⊣ i^{∗} [figure] \end{matrix}

V = !_{Γ}^{∗}b^{∗}W \frac{⊂}{}

C^{c_{⊔} }  \overline{!_{C}} B = \{⊥\} \begin{matrix}b_{⊔} &  \\ ⊣ {!_{Γ} \atop } \end{matrix}  \overline{!_{B}}^{!_{Γ}  \overline{}}\{⊥\}^{^{⊔} }  S = Σ [figure: b_{!} = !_{Γ}^{∗}]⊣ [figure: b^{∗}] ⊣ ∀_{b}

Using Remark 1.2, put

V = !_{Γ}^{∗}b^{∗}W = Γ | (⊥ ∈ W) ⊂ Γ
Z = p^{∗}i^{∗}W ⊂ U.

I claim that U ∩ V = Z as in Remark 3.2:

U ∩ V = j^{∗}!_{Γ}^{∗}b^{∗}W = p^{∗}i^{∗}!_{Γ}^{∗}b^{∗}W ⊂ p^{∗}i^{∗}W = Z ⊂ U.

The first equality is just j^{∗} ≡ U ∩ (−) applied to the definition of V. The second uses the fact that !_{Γ} · j and !_{Γ} · i · p are maps to the terminal object, so must be equal. The containment follows from Definition 2.5, which says that !_{Γ}^{∗} · b^{∗} = b_{!} · b^{∗} ≤ id_{Γ}, whilst p^{∗} · i^{∗} preserves order.

Hence we have open subspaces of X with the following sublattice of inclusions:

U ∪ V

Y ............

V ............  U

Z^{.................................}

U ∩ V

By modularity, there is a unique Y such that V ⊂ Y ⊂ U ∪V and Z = Y ∩U, namely Y = V ∪Z (cf. Remark 3.2).

Remark 5.2 (Continuation of the proof.) I claim that this construction yields Y = f^{∗}W as required. With W = X, it gives V = ∅ (by Lemma 1.3(a)) and Y = U ∪ V = U as required for the pullback condition. Similarly, W = X_{⊥} and ∅ give Y = Γ and ∅, and it is also easy to see that f^{∗} : W ↦ Y preserves unions. What is more difficult to show is that binary intersections are preserved: attacking it with the blunt instrument of distributivity is not a good idea when the issue is modularity. In the obvious notation,

V_{1} ∩ V_{2} ⊂ Y_{1} ∩ Y_{2} ⊂ U ∪ (V_{1} ∩ V_{2}) and (Y_{1} ∩ Y_{2}) ∩ U = Z_{1} ∩ Z_{2}

(albeit using distributivity), so Y_{1} ∩ Y_{2} uniquely does the job of Y.

Remark 5.3 (Continuation of the proof.) Suppose conversely that a total extension f exists, and put Y = f^{∗}W. Commutativity of the bold square says that Y ∩ U = Z ⊂ U, where V and Z are defined as above. Then

V = !_{Γ}^{∗}b^{∗}W = f^{∗}!_{Γ}^{∗}b^{∗}W ⊂ f^{∗}W = Y

by the same argument as for U ∩ V ⊂ Z above, using monotonicity of f^{∗} and Definition 2.5. From Lemma 1.3(c) and Definition 2.5, and since ∃_{i}i^{∗}W ⊂ X,

W = ∃_{i}i^{∗}W ∪ b_{!}b^{∗}W ⊂ X ∪!_{Γ}^{∗}b^{∗}W,

and f^{∗} preserves this union, so

Y = f^{∗}W ⊂ f^{∗}X ∪ f^{∗}!_{Γ}^{∗}b^{∗}W = U ∪ V.

Again, by modularity, we must have Y = Z ∪ U. □

Remark 5.4 We have found f^{∗} by means of the composite construction

[figure: W; (V, Z); Y = U ∪ V; (V, Y); Y; Σ^{X_{⊥}}; (p^{∗} · i^{∗}, !_{Γ}^{∗} · b^{∗}); E_{U}; F_{U}; π_{1}; Σ^{Γ}]

where the order-isomorphism between

E_{U} = {(V, Z) ∈ G^{2} | U ∩ V ⊂ Z ⊂ U} and F_{U} = {(V, Y) ∈ G^{2} | V ⊂ Y ⊂ U ∪ V }

is that stating the the modular law in Definition 3.3. In fact, E_{U} and F_{U} are (isomorphic) frames, and the maps displayed are frame homomorphisms. It is this construction that we shall adapt to abstract Stone duality in Section 7.

Remark 5.5 The modular law has a sting in its tail. It would be a little prettier to use the isomorphic three-variable lattices

E = {(U, V, Z) | U ∩ V ⊂ Z ⊂ U} and F = {(U, V, Y) | V ⊂ Y ⊂ U ∪ V },

but unfortunately they are not modular, except in the trivial case G = 1. So they cannot be frames, or algebras for abstract Stone duality monad. This is because E contains the following as a sublattice (Example 3.4(a)), where ⊤⊤⊥ is excluded by U ∩ V ⊂ Z, whilst ⊥⊥⊤ and ⊥⊤⊤ fail Z ⊂ U (⊥⊤⊥ in E becomes ⊥⊤⊤ in F).

⊤⊤⊤

⊤⊥⊤
⊥⊤⊥
⊤⊥⊥

⊥⊥⊥

6 Comma squares of algebras in ASD

Having described the lift for locales in a way that does not depend on the unacceptable features of the traditional axiomatisation, we now begin to adapt the argument to abstract Stone duality. Despite the switch to the more abstract language, you can continue to read this for locally compact locales, as they form a model of the axioms.

Definition 6.1 Abstract Stone duality says, briefly, that the category S of spaces satisfies the following properties:

(a) S has products and an object Σ of which all powers Σ^{X} exist, and moreover the contravariant adjunction Σ^{(−)} ⊣ Σ^{(−)} is to be monadic. We also assume that idempotents (retracts) split. This idea is developed in [A, B], and exploited in the next section.

(b) Σ is an internal distributive lattice satisfying the Phoa principle (Definition 2.3): the order relation defined by the lattice structure is Σ^{≤} ≅ Σ^{Σ}. This has the effect that Σ classifies both open and closed subspaces[C].

(c) There is a natural numbers object ℕ, which is overt, i.e. admits an existential quantifier ∃_{ℕ} : Σ^{ℕ} → Σ. We use this to define general recursion in Section 8.

(d) The Scott principle: for any F : Σ^{Σ^{ℕ}} and ϕ : Σ^{ℕ},

F ϕ = ∃n. F (λm. m < n) ∧ ∀m < n. ϕ[m].

This axiom is exploited in [E], but not used in this paper: by withholding it, we see how powerful its finitary version, the Phoa principle, is in explaining certain apparently infinitary aspects of topology.

In this section we simply recall the main results from [C, Sections 3 and 5], in particular the definitions of open and closed subspaces. Using this, we construct the lift as a comma square (cf. Sections 1 and 2 above). The proof involving modularity that this gives the partial map classifier (cf. Section 5) will be given in the next section.

Besides saying that Σ is a distributive (and ā fortiori modular) lattice, the Phoa principle can be resolved into three parts, on which the following results respectively depend [C, Proposition 5.7].

Remark 6.2 In the category so axiomatised, the objects and hom-sets inherit the order from Σ. In fact, most of the objects that we consider in the proof are algebras, and are in any case retracts of powers of Σ. The first part of the Phoa principle is that all maps Σ → Σ be monotone [C, Lemma 5.2]. It follows that the functor Σ^{Σ^{(−)}}, which we abbreviate as Σ^{2}(−), preserves this order. □

Corollary 6.3 G^{2} and G^{≤} carry Eilenberg–Moore algebra structures for the monad in Definition 6.1(a), such that the inclusion

G^{Σ} ≅ G^{≤} = {(x, y) | x ≤ y} ↣ G^{2}

is an Eilenberg–Moore homomorphism. □

Corollary 6.4 The diagonal G → G^{≤} by x ↦ (x, x) is also a homomorphism. □

The second part of the Phoa principle is called the Euclidean principle. It characterises dominances (“subobject classifiers”) in the context of the monadic axiom, i.e. the fact that the characteristic map of an open subset is unique [C, Section 3].

In the next two results, u ∈ G = Σ^{Γ} is a global element, u : 1 → Σ^{Γ}.

Proposition 6.5 In the retraction,

G [figure: i^{∗}; ⊤; ∃_{i}] A = (G ↓ u) = {a | a ≤ u} by (−) ∧ u,

A is an algebra such that i^{∗} is a homomorphism and ∃_{i} satisfies the Frobenius law, so i is an open inclusion [C, Proposition 3.11]. Proof The map i^{∗} is the inverse image for the inclusion of the open subspace U, which is an equaliser:

[figure: U; ⊂; i; Γ; ⊂; x ↦ ⟨x, ⊤⟩; x ↦ ⟨x, (x ∈ U)⟩; Γ × Σ]

[figure: (G ↓ u); \underline{i^{∗} ≡ (−) ∧ u}; ⊤; ∃_{i}; G = Σ^{Γ}; W ↦ λxσ. σ ∧ (x ∈ W); Σ^{Γ×Σ}]

The corresponding coequaliser of topologies and homomorphisms (exists because it) is split by the Scott-continuous maps shown. The relevant equation in Beck’s theorem is given by the Euclidean principle, and the Frobenius law is a third way of seeing the same thing [C, Lemma 3.3]. □

The third part of the Phoa principle is the lattice dual of the Euclidean principle, and does the same for closed subspaces:

Proposition 6.6 In the retraction

G [figure: c^{∗}; ⊥; ∀_{c}] S = (u ↓ G) = {s | s ≥ u} by (−) ∨ u,

S is an algebra such that the map c^{∗} is a homomorphism and ∀_{c} satisfies the dual Frobenius law, so c is a closed inclusion [C, Corollary 5.6]. □

Now we are ready to construct the lift X_{⊥} by forming H = Σ^{X_{⊥}} as a comma square involving A = Σ^{X}, just as in Definition 2.5. Here (A, α) may any Eilenberg–Moore algebra for the monad — the whole point of the monadic adjunction is that, to define a space X, it is necessary and sufficient to construct Σ^{X}. This is the most general kind of comma square that we shall need to construct directly in abstract Stone duality.

Lemma 6.7 The object H = ℓ ↓ A = {(s, a) | ℓ(s) ≤ a} ⊂ Σ × A exists, being the image of the closure operation (s, a) ↦ (s, ℓ(s) ∨ a), where ℓ : Σ → A is the unique homomorphism (that is, !_{X}^{∗} when A = Σ^{X}). □

Proposition 6.8 H is the comma object ℓ ↓ A in the Eilenberg–Moore category.

Σ^{2}H  \overline{}Σ^{2}A

[figure: H; π_{0}; θ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; A; α]

[figure: Σ^{2}Σ; Σ^{2}A; ↙]

[figure: Σ; π_{1}; ℓ; η_{1}^{∗}; A; id; ↙; α]

Proof In the construction of the lift, ℓ is a homomorphism, although it would be enough to have ℓ · η_{1}^{∗} ≤ α · Σ^{2}ℓ in this construction. Then we have a lax square from Σ^{2}H to A, and hence a mediator θ : Σ^{2}H → H that makes the left and top faces of the cube commute. These say that π_{0} and π_{1} are Eilenberg–Moore homomorphisms. By uniqueness of mediators from a similar lax square involving Σ^{4}H, (H, θ) is an algebra. A similar argument shows that the mediator from any other lax square involving homomorphisms Δ → A and Δ → Σ is also a homomorphism. □

7 The modular law and lifting in ASD

The remaining issue is to show that the map f^{∗} in Theorem 5.1 that we have claimed to be the inverse image of the total extension in the partial map classifier) is in fact a homomorphism of Eilenberg–Moore algebras in abstract Stone duality formulation, cf. Remark 5.2.

This means that we have to show that a certain equation is valid. Equational reasoning is, however, notoriously difficult to follow — and therefore prone to error — especially when it is based on the modular law. (Our equation involves composition and the functor Σ^{(−)}, which may be defined in terms of the λ-calculus, so some people would want to express it as a string of stepwise equations and β-reductions, but I rather doubt whether they would succeed in doing this correctly, let alone informatively.) For this reason, it is vital to identify the conceptual structure behind the symbol-pushing, and in particular to employ commutative diagrams to record the both types of the sub-formulae and the names and roles of the equational laws being invoked.

Much of the original body of results about monads [Eck69, BW85] depends on the availability of equalisers and coequalisers of arbitrary pairs of functions between sets, or of homomorphisms between algebras, and is therefore of no use in abstract Stone duality. This is not the case for the theorem of Jon Beck that characterises monadic adjunctions in terms of “U-split coequalisers” [Tay99, Theorem 7.5.9] [BW85, Section 3.3] [ML71, Section VI 7], so we rely very heavily on this result, and are forced to learn how to find such coequalisers when we need them. An account of how Beck’s theorem provides certain subspaces is given in [B, Section 3].

As well as U-split or absolute coequalisers, a certain species of absolute pushout also shows up rather commonly when we start looking [B, Section 7] (Absolute means that the universal property, being given by equations, is preserved by any functor.)

The objects and maps in the following result are given the names that they have in the Karoubi construction, although the letters i, j, k, p, q and r now play different roles from those earlier in the paper.

Lemma 7.1 Let e and e′ be idempotents on an object in any category that has splittings of idempotents, such that the composites e ; e′ and e′ ; e are also idempotent (but not necessarily equal), so we have the equations

e; e = e,  e′ ; e′ = e′,  e; e′ ; e; e′ = e; e′  and  e′ ; e; e′ ; e = e′ ; e.

Then the objects E and F that split the idempotents e; e′ and e′ ; e are isomorphic.

id

[figure: e; j = e; q = e; e′; q′ = e′; j′ = e′]

[figure: E ≡ e; e′; i = e; e′ ; e; p = e; e′; b = e; e′ ; e; ≅; \underline{a = e′ ; e; e′}; k = e; e′; s = e′ ; e; e′; e′ ; e ≡ F; p′ = e′ ; e; i′ = e′ ; e; e′; k′ = e′ ; e; s′ = e; e′ ; e]

Moreover, we have the equations:

(7.6)  k ; s = id_{E} = e; e′  (7.9) b = a^{−1} = e; e′ ; e
(7.6) j ; q′ = p; k = e; e′  (7.11) i = b; k′ = e; e′ ; e

(7.10) k′ ; s′ = id_{F} = e′ ; e  (7.8) i′ = a; k = e′ ; e; e′
(7.9)  a = k′ ; p = e′ ; e; e′  (7.8) s′ = p; b = e; e′ ; e  □

Remark 7.2 With h and r both given by e; e′ ; e, we also have split equalisers and coequalisers,

[figure: F; k′; .; .; .; .; .; .; .; s′...........; e; j; h; .; .; .; .; .; .; .; q...........; id; id; q; r; .; .; .; .; .; .; .; .; .; j; .; .; .; .; .; .; .; .; .; .; e; p; .; .; .; .; .; .; .; .; .; i; .; .; .; .; .; .; .; .; .; .; E]

together with the versions with the primes the other way. From the coequaliser (on the right) it follows that E (or F) is the absolute pushout of the surjections in Lemma 7.1. Beware, however, that the diamonds of monos do not commute, so we don’t have a pullback (unless e;e′;e = e;e′). □

The idempotents e and e′ that interest us are defined for any internal lattice (G, ∧, ∨) in any category with finite products, essentially by

G × G  [figure: ⟨π_{0}, ∨⟩; ⟨π_{0}, ∧⟩] G × G,

though we shall use a rather less pedantic notation than this. The familiar symbolic notation is justified, at least for the morphisms, in any category with finite products [Tay99, Section 4.6], with the convention that morphisms act as the identity on those variables that occur in the names of both their source and target but not in the name of the morphism. The objects exist in abstract Stone duality because they are defined by retracts of G^{2} or G^{3}, where G = Σ^{Γ}.

Proposition 7.3 Let G be an internal modular lattice any a category with finite products and splittings of idempotents. Then the following diagram has the properties listed in Lemma 7.1.

{(u, v, t)} = G^{3}

[figure: {(u, v, y) | v ≤ y}; q = [t ∨ v/y] ⊥; j = [y/t]; {(u, v, z) | z ≤ u}; q′ = [t ∧ u/z] ⊤; j′ = [z/t]]

E = \{(u, v, z) | u ∧ v ≤ z ≤ u\} \begin{matrix}\begin{aligned}i = [v ∨ z/y] \\ &  \end{aligned} &  \\ ⊣ [figure: p = [u ∧ y/z]] \end{matrix} [figure: b = [v ∨ z/y]; ≅; \underline{a = [u ∧ y/z]}] [figure: \begin{matrix}⊥ \\ k \end{matrix}] [figure: [u ∧ (v ∨ z)/z]] \{(u, v, y) | v ≤ y ≤ u ∨ v\} = F^{[figure: p′ = [v ∨ z/y]]⊣ \begin{matrix}i′ = [u ∧ y/z] \\  \end{matrix}}[figure: \begin{matrix}⊤ \\ k′ \end{matrix}] [figure: [(u ∧ y) ∨ v/y]]

Proof Our idempotents are, more precisely,

e : (u, v, t) ↦ (u, v, t ∨ v)  and  e′ : (u, v, t) ↦ (u, v, t ∧ u),

so the equation e; e′ = e; e′ ; e; e′ amounts to

u ∧ (t ∨ v) = u ∧ ((u ∧ (t ∨ v)) ∨ v),

which is one of the many versions of the modular law, as is its dual (Remark 3.5). Since the name of each map in the Karoubi notation consists of its source (which acts as the identity) followed by (usually just of one of) e or e′, it is not too difficult to translate Lemma 7.1 into lattice notation. □

Remark 7.4 The simpler equation

e; e′ ; e = e′ ; e, which is u ∧ ((t ∧ u) ∨ v) = u ∧ (t ∨ v),

expresses distributivity and, of course, implies the ones used above. However, this is not the same as the equation mentioned in Remark 7.2 that would make the diamond of monos commute, which only holds when G = 1. In fact, the pullback of i and j is {(u, v, t) | v ≤ t ≤ u}.

Remark 7.5 Because of Remark 5.5, we must restrict the diagram by fixing a global element u ∈ G. The following maps are then lattice homomorphisms (indeed, frame homomorphisms as they are also continuous): we shall show that these objects are Eilenberg–Moore algebras for our monad and that the maps are homomorphisms in that sense too.

{(v, t)} = G^{2}

[figure: G^{≤} ≡ {(v, y) | v ≤ y}; j (6.3); h (7.12); {(v, z) | z ≤ u} ≡ G × (G ↓ u); q′ (6.5)]

E_{u} ≡ \{(v, z) | u ∧ v ≤ z ≤ u\} \begin{matrix}\begin{aligned}i (7.11) \\ &  \end{aligned} &  \\ ⊣ [figure: p (7.6)] \end{matrix}  [figure: b (7.9); ≅; \underline{a (7.9)}] [figure: k (7.6)] \{(v, y) | v ≤ y ≤ u ∨ v\} ≡ F_{u} [figure: i′ (7.8)] [figure: s′ (7.8)] [figure: k′ (7.10)]

The symmetry has been lost: h′, p′, q, r, r′ and s don’t preserve ∧, whilst j′ doesn’t preserve ⊤.

Lemma 7.6 There is a unique Eilenberg–Moore algebra structure on the object E_{u} for which p : G^{≤} → E_{u} and k : E_{u} → G × (G ↓ u) are homomorphisms.

[figure: Σ^{2}(G^{≤}); Σ^{2}p; Σ^{2}E_{u}; Σ^{2}k; Σ^{2}(G × (G ↓ u)); G^{≤}; p; E_{u}; . . . . . . . . . . . . . . . .; k; G × (G ↓ u)]

Proof The maps G^{≤} ^{j} G^{2} ^{q′} G × (G ↓ u) are homomorphisms by Corollary 6.3 and Proposition 6.5. Then p; k is the image factorisation of the composite, indeed with p split epi and k split mono. The structure map on E_{u} is therefore given by composition, so that p and k are also homomorphisms. The Eilenberg–Moore equations for the algebra E_{u} are justified in a similar way using Σ^{4}. □

Corollary 7.7 E_{u} can be expressed as a comma square of algebras,

Σ^{X_{⊥}}  \overline{}A = Σ^{X}

[figure: E_{u}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; G ↓ u ∋ z]

S = Σ \begin{aligned}b^{∗} \\ &  \end{aligned}

[figure: v ∈ G; (−) ∧ u; !^{∗}; G ↓ u; id; ↗]

and the mediator Σ^{X_{⊥}} → E_{u} provides the first part, W ↦ (V, Z), of the construction in Section 5. Proof E_{u} is clearly a comma square of objects, but the homomorphism k makes it a subalgebra of G × (G ↓ u). □

Lemma 7.8 By the same method, the object F_{u} = {(v, y) | v ≤ y ≤ u ∨ v} carries a unique structure for which s′ : G^{≤} → F_{u} and i′ : F_{u} → G × (G ↓ u) are homomorphisms. In fact it is unique for either of them to be a homomorphism. □

Lemma 7.9 Similarly, a and b are isomorphisms of algebras (“monadic forgetful functors reflect invertibility”). □

The factorisation method doesn’t help to show that the inclusions i : E_{u} G^{≤} and k′ : F_{u} G^{≤} are homomorphisms. (We shall need k′; π_{1} to project out the result y.) Although k′ is the equaliser of j and h by Remark 7.2, we do not yet know that h is a homomorphism.

Lemma 7.10 The following square is a pullback of homomorphisms.

\begin{matrix}\{(v, y) | v ≤ y\} = G^{≤} & \overline{\begin{matrix}6.6 : (c^{∗})^{≤} \\ [u ∨ v/v′, u ∨ y/y′] \end{matrix}} & (u ↓ G)^{≤} = \{(v′, y′) | u ≤ v′ ≤ y′\} \\ \{(v, y) | v ≤ y ≤ u ∨ v\} = F_{u} & [figure: k′]⊣ [figure: s′ = [(u ∧ y) ∨ v/y]] . . . . . . . . . . . . . . . . . . . . . . & \overline{[u ∨ v/v′]} & u ↓ G = \{v′ | u ≤ v′\} & [figure: 6.4 Δ] \end{matrix}

In particular, the inclusion k′ : F_{u} G^{≤} is a homomorphism. Proof First we have to show that the square is a pullback of functions, but any test square with (v, y) : Δ → G^{≤} and v′ : Δ → u ↓ G satisfies

v ≤ y ≤ u ∨ y = v′ = u ∨ v

since v ≤ y ≤ u ∨ v iff v ≤ y & u ∨ v = u ∨ y.

Then, given the known structure on the other three objects and since “monadic forgetful functors create pullbacks”, there is a unique structure on F_{u} for which the square is a pullback of homomorphisms.

Using this (new) structure on F_{u}, the homomorphism s′ : G^{≤} → F_{u} mediates to the pullback from the commutative square involving id : G^{≤} → G^{≤} and c^{∗} · π_{0} = [u ∨ v/v′] : G^{≤} → u ↓ G, the latter being a homomorphism by Proposition 6.6.

This is the same algebra structure as in Lemma 7.8, because there is only one such structure that makes s′ a homomorphism. □

Lemma 7.11 i = b; k′ = [v ∧ z/y] : E_{u} → G^{≤} is a homomorphism by composition. □

Lemma 7.12 h = p ; i ; j = e ; e′ ; e = [(u ∧ y) ∨ v/t] : G^{≤} G^{2} is a homomorphism by composition. □

Theorem 7.13 Lifting provides the partial map classifier in abstract Stone duality. Proof The construction and proof are the same as in Theorem 5.1, where W ↦ (V, Z) ↦ (V, Y) ↦ Y is a composite of maps that we have just shown to be homomorphisms. □

Remark 7.14 The spaces and continuous maps that correspond to the algebras and homomorphisms that we have used in this section are as illustrated:

\begin{matrix}U & U \\ C & C \end{matrix} Γ + Γ = Γ × 2

[figure: U; U; C; C; Γ × Σ; Γ + U; ⊃; \begin{matrix}U & U \\ C \end{matrix}]

[figure: \begin{aligned}& U \\ U \\ C \end{aligned}]

Each linked pair U–C denotes a copy of the original space Γ, whilst U–U and U U with or without a link denote U × Σ and the disjoint union (U × 2) respectively. Of the two parallel surjections, one (whose inverse image map is j) matches the four parts in the obvious way, whilst the other (corresponding to h) sends both Cs to the lower one. Similarly, the inclusion of the three-part object at the bottom sends C to the lower copy.

8 General recursion

As an application of lifting, we construct the search or minimalisation operator μ : (2_{⊥})^{ℕ} → ℕ_{⊥} for general recursion. Here we regard this as a problem in domain theory, and not as part of the construction of the recursion-theoretic halting set that we needed in Section 4. Besides the obvious uses of lifting in the definition, gluing ideas are used again towards the end of the proof. This construction is included in this paper, rather than in a later one on domain theory or recursion theory [F], in order to emphasise that it is done without an additional fixed point axiom.

We do, of course, now assume that ℕ admits primitive recursion, although we actually only need this at type Σ^{ℕ}. In fact, the properties of ℕ that we use are:

Lemma 8.1 ℕ carries a binary relation <_{ℕ} such that

(a) n, m : ℕ ⊢ n <_{ℕ} m ∨ n =_{ℕ} m ∨ m <_{ℕ} n and

(b) {m | m < n} is compact, i.e. we may form ∀m < n.ϕ[m]. □

We also use the existential quantifier ∃_{ℕ} : Σ^{ℕ} → Σ, so ℕ is overt [C, Definition 7.7]. These two axioms of abstract Stone duality, together with the more basic ones that we have used so far (Remark 6.1), can be seen as universal properties, which the traditional definition of μ cannot.

Recall that the idea of μ(f) is that it runs f(0), f(1), ..., returning as its value the first n for which f(n) returns an affirmative result. All f(m) for m < n must have returned definite negative results, and in particular f(m) must terminate for each m ≤ n. If we know ∃n. f(n) = 0 then [A, Lemma 9.11] defines μ(f) using description:

μ(f) = the n. f(n) = 0 ∧ ∀m < n. f(m) > 0.

In this paper we have constructed the partial map classifier. This allows us to remove the existential hypothesis on f, makin μ(f) partial, and f itself may also be a partial function.

Traditionally, 0 ∈ ℕ denotes affirmative, and any other (i.e. positive) number denotes negative. Instead, we consider f : ℕ → 2_{⊥}, as there are only two definite results, and ℕ_{⊥} does not have a convenient representation in the absence of the fixed point axiom.

In fact, we shall represent f : ℕ → 2_{⊥} by (ϕ, ψ) ∈ Σ^{ℕ} × Σ^{ℕ} such that

T (ϕ, ψ) ≡ ∃n. ϕ[n] ∧ ψ[n] = ⊥,

and so we begin by showing that 2, 2_{⊥}, (2_{⊥})^{⊤} ≅ (2^{⊤})_{⊥} and Σ × Σ are related in the expected way.

Lemma 8.2 2_{⊥} is the closed subspace {ϕ, ψ | ϕ ∧ ψ = ⊥} ^{⊏} Σ × Σ, and 2_{⊥}^{⊤} ≅ Σ × Σ.

[figure: 2_{⊥}; 1; Σ × Σ; ⊓; ∧; Σ; ⊥]

Proof This could be shown by lattice-theoretic manipulation of the double comma object that provides the topology on 2_{⊥}^{⊤}, but we prove instead that Σ×Σ has the universal property of (2_{⊥})^{⊤}. We must show that maps (ϕ, ψ) : Γ → Σ × Σ correspond to partial maps p : Γ ⇀ 2 whose domain of definition is locally closed, i.e. an open subset D of a closed subset C ⊂ Γ.

D = W \ U  \overline{p} 2

[figure: C = Γ \ U; ∩; 2_{⊥}; ∩]

[figure: Γ; ⊓; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; (ϕ, ψ); Σ × Σ; ⊓]

As usual, D = W ∩ C for some open subset W ⊂ Γ, and the topologies on C and D are U ↓ G and U ↓ G ↓ W, where U is the open complement of C.

The partial map p is determined by two (cl)open subsets of D, which are the restrictions to D of open subsets Φ, Ψ ⊂ Γ such that

Φ ∩ Ψ = U ⊂ Φ, Ψ ⊂ U ∪ W = Φ ∪ Ψ,

which together provide a map (ϕ, ψ) : Γ → Σ × Σ. Conversely, U, W, C, D and p : D → 2 may be recovered from (ϕ, ψ).

When C = Γ, so U = ∅, the domain of definition is open, and p : D ⇀ 2 is a partial map of the kind treated in Definition 2.1, so the corresponding subspace {(ϕ, ψ) | ϕ ∧ ψ = ⊥} has the universal property of 2_{⊥}. □

Corollary 8.3 (2_{⊥})^{ℕ} is the closed subspace {ϕ, ψ | (∃n. ϕ[n] ∧ ψ[n]) = ⊥} of Σ^{ℕ} × Σ^{ℕ}. Proof Using [C, Proposition 7.10],

[figure: (2_{⊥})^{ℕ}; 1; 1; Σ^{ℕ} × Σ^{ℕ}; ⊓; ∧; Σ^{ℕ}; ⊥; ∃; Σ; ⊥]

□

Remark 8.4 Similarly, ℕ_{⊥} = {θ | D(θ) = ⊥} ⊂ Σ^{ℕ},

[figure: ℕ_{⊥}; {⊥}; Σ^{ℕ}; ⊓; D; Σ]

where D(θ) says that θ has at least two distinct elements (see below). But this is only valid if we assume the fixed point axiom, that F (λn. ⊤) = ∃m. F (λm. m < n) for all F : Σ^{ℕ} → Σ.

This axiom would make the lower right square below a pullback too. The big square P ⇉ Σ×Σ commutes because D · S ≤ T, so the mediator to the pullback ℕ_{⊥} provides μ_{0} and μ.

We shall show that μ can be constructed without such an assumption.

Notation 8.5 Let S(ϕ, ψ) = σ = λn. σ_{n} and T (ϕ, ψ) = τ = ∃n. τ_{n}, where

σ_{n}  = ϕ[n] ∧ ∀m < n. ψ[m]
τ_{n}  = ϕ[n] ∧ ψ[n]
D(θ) = ∃nm. θ[n] ∧ θ[m] ∧ (n < m).

Then we shall define μ by means of the diagram

[figure: 1; P; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; μ_{0}; ℕ; 1]

[figure: Σ; ⊤; (2_{⊥})^{ℕ}; ∩; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; μ; ℕ_{⊥}; ∩; Σ; ⊤]

[figure: Σ × Σ; ⟨id, ⊥⟩; ⟨∃ · S, T ⟩; Σ^{ℕ} × Σ^{ℕ}; ⊓; S; Σ^{ℕ}; ⟨∃, D⟩; Σ × Σ; ⟨id, ⊥⟩]

We leave the interested reader to show that the lower middle square is not a pullback in any circumstances, and that P ≅ (2_{⊥})^{ℕ} × ℕ.

Lemma 8.6 {n} ∧ σ_{n} ≤ σ, D · S ≤ T and σ ∧ σ_{n} ∨ τ_{n} ≤ {n} ∨ τ. Proof

({n} ∧ σ_{n})(m) = (m =_{ℕ} n) ∧ ϕ[n] ∧ ∀m < n. ψ[m]
≤ ϕ[m] ∧ ⋀_{m′<m} ψ[m′]
= σ(m)

DS(ϕ, ψ) = ∃mn. ϕ[n] ∧ ∀m < n. ψ[m] ∧ ϕ[m] ∧ ⋀_{m′<m} ψ[m′] ∧ (n < m)
≤ ∃n. ϕ[n] ∧ ψ[n]
= T (ϕ, ψ).

Similarly, using trichotomy of <_{ℕ} (Lemma 8.1(a)) and with k = min(n, m),

(σ_{n} ∧ σ ∨ τ_{n})(m) = (ϕ[n] ∧ ∀m < n. ψ[m] ∧ ϕ[m] ∧ ⋀_{m′<m} ψ[m′])
∨ (ϕ[n] ∧ ψ[n])
≤ (n =_{ℕ} m) ∨ ∃k. ϕ[k] ∧ ψ[k]
= (n =_{ℕ} m) ∨ τ  □

Remark 8.7 The inclusions P  Σ^{ℕ} × Σ^{ℕ} and ℕ  Σ^{ℕ} are Σ-split:

(a) P is locally closed, so by Section 6, Σ^{P} splits the idempotent H : G ↦ (G ∧ ∃ · S) ∨ T on Σ^{Σ^{ℕ}×Σ^{ℕ}};

(b) Σ^{ℕ} splits J : F ↦ λθ. ∃n. F {n} ∧ θ[n] on Σ^{Σ^{ℕ}} [C, Proposition 7.12]. Then we define μ_{0} : P → ℕ by constructing the homomorphism Σ^{μ_{0}} as a map between splittings of idempotents, or as the composite of the other three sides of the square:

[figure: P; Σ^{P}; Σ^{Σ^{ℕ}×Σ^{ℕ}}; Σ^{ℕ} × Σ^{ℕ}]

[figure: ℕ; μ_{0}; . . . . . . . . . . . . . . . . .; Σ^{ℕ}; Σ^{μ_{0}}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; θ ↦ λϕ. ∃n. ϕ[n] ∧ θ[n]; \underline{λn. F \{n\} ← F}; Σ^{Σ^{ℕ}}; Σ^{S}; Σ^{ℕ}; S]

Σ^{μ_{0}} is an Eilenberg–Moore homomorphism because the maps Σ^{Σ^{ℕ}} → Σ^{Σ^{ℕ}} × Σ^{Σ^{ℕ}} → Σ^{P} are homomorphisms and Σ^{Σ^{ℕ}} → Σ^{ℕ} is a quotient algebra.

What we have to check is:

Lemma 8.8 H · Σ^{S} = H · Σ^{S} · J. Proof Apply them to F ∈ Σ^{Σ^{ℕ}} and ϕ, ψ ∈ Σ^{ℕ}. The left hand side is

L = H · Σ^{S}(F)(ϕ, ψ) = HF S(ϕ, ψ) = (F ∧ ∃)σ ∨ τ
= F (λn. ϕ[n] ∧ ∀m < n. ψ[m]) ∧ (∃n. ϕ[n] ∧ ∀m < n. ψ[m])
∨ (∃n. ϕ[n] ∧ ψ[n])
= ∃n. F σ ∧ σ_{n} ∨ τ_{n}

using Frobenius, whilst the right hand side is

R = H · Σ^{S} · J(F)(ϕ, ψ) = H(JF)S(ϕ, ψ) = (JF ∧ ∃)σ ∨ τ
= (∃n. F {n} ∧ ϕ[n] ∧ ∀m < n. ψ[m]) ∧ (∃n. ϕ[n] ∧ ∀m < n. ψ[m])
∨ (∃n. ϕ[n] ∧ ψ[n])
= ∃n. F {n} ∧ σ_{n} ∨ τ_{n}

Writing ∃n. L_{n} and ∃n. R_{n} for these expressions, we show that R_{n} ≤ L_{n} ≤ ∃n. R_{n}. For the first,

F {n} ∧ σ_{n} = F ({n} ∧ σ_{n}) ∧ σ_{n} ≤ F σ ∧ σ_{n}

by Lemma 8.6 and since F is monotone and satisfies the Euclidean principle. For the second,

F σ ∧ σ_{n} ∨ τ_{n} = F (σ ∧ σ_{n} ∨ τ_{n}) ∧ σ_{n} ∨ τ_{n}  Phoa
≤ F ({n} ∨ τ) ∧ σ_{n} ∨ τ_{n}  Lemma 8.6
≤ F ({n} ∨ τ) ∧ σ_{n} ∨ τ
= F {n} ∧ σ_{n} ∨ τ  dual Euclid
≤ ∃n. R_{n}  □

Theorem 8.9 There is a uniquely defined map μ : (2_{⊥})^{ℕ} → ℕ_{⊥} making the diagram in Notation 8.5 commute.

[figure: P; μ_{0}; ℕ; {−}; Σ^{ℕ}]

Σ^{ℕ} × Σ^{ℕ}^{S  \overline{}}

[figure: (2_{⊥})^{ℕ}; ∩; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; μ; ⊏; ℕ_{⊥}; ∩; {−}_{⊥}; (Σ^{ℕ})_{⊥}; ∩]

[figure: Q; ⊔; 1; ⊥; 1; ⊥]

Proof We have already constructed μ_{0} to make the upper quadrilateral commute, and then μ : (2_{⊥})^{ℕ} → ℕ_{⊥} is defined by lifting, which makes the upper left square a pullback. The question is whether the maps (2_{⊥})^{ℕ} ⇉ Σ^{ℕ} × Σ^{ℕ} agree (the lower middle square in Notation 8.5).

Let Q ⊂ Σ^{ℕ} × Σ^{ℕ} be the closed subspace classified by ∃ · S = ⊥ and T = ⊥, so Q is the closed complement of P ⊂ (2_{⊥})^{ℕ}. By construction, μ takes the value ⊥ ∈ ℕ_{⊥} on Q, and this is carried to λn. ⊥ ∈ Σ^{ℕ}, which is also the value of S on Q.

Thus the diagrams P ⇉ Σ^{ℕ} and Q ⇉ Σ^{ℕ} commute, so maps agree on (2_{⊥})^{ℕ} by Theorem 3.9. □

References

[AAB80] Ahmad Abd-Allah and Ronald Brown. A compact-open topology on partial maps with open domain. Journal of the London Mathematical Society (2), 21:480–6, 1980.

[AGV64] Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, editors. Séminaire de Géometrie Algébrique, IV: Théorie des Topos, number 269–270 in Lecture Notes in Mathematics. Springer-Verlag, 1964. Second edition, 1972.

[BB78] Peter Booth and Ronald Brown. Spaces of partial maps, fibred mapping spaces and the compactopen topology. General Topology and its Applications, 8:181–195, 1978.

[BW85] Michael Barr and Charles Wells. Toposes, Triples and Theories. Number 278 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, New York, 1985.

[DP90] Brian Davey and Hilary Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge, U.K., 1990.

[DT87] Roy Dyckhoff and Walter Tholen. Exponentiable maps, partial products and pullback complements. Journal of Pure and Applied Algebra, 49:103–116, 1987.

[Eck69] Beno Eckmann, editor. Seminar on Triples and Categorical Homology Theory, number 80 in Lecture Notes in Mathematics. Springer-Verlag, 1969.

[Jib98] Mamuka Jibladze. Lower bagdomain as a glueing. Proc. Razmadze Math. Inst., 118:31–41, 1998.

[Joh] Peter Johnstone. locmt.

[Joh77] Peter Johnstone. Topos Theory. Number 10 in London Mathematical Society Monographs. Academic Press, 1977.

[Joh82] Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh91] Peter Johnstone. Partial products, bagdomains and hyperlocal toposes. In Michael Fourman, Peter Johnstone, and Andrew Pitts, editors, Applications of Categories in Computer Science, volume 177 of LMS Lecture Note Series, pages 315–339. Cambridge University Press, 1991.

[ML71] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

[Nie82] Susan Niefield. Cartesianness: Topological spaces, uniform spaces and affine varieties. Journal of Pure and Applied Algebra, 23:147–167, 1982.

[Pas65] Boris Pasynkov. Partial topological products. Transactions of the Moscow Mathematical Society, 13:153–271, 1965.

[Pho90a] Wesley Phoa. Domain Theory in Realizability Toposes. PhD thesis, Cambridge, 1990. Available as University of Edinburgh Dept. of Computer Science report CST-82-91 and ECS-LFCS-91-171.

[Pho90b] Wesley Phoa. Effective domains and intrinsic structure. In Logic in Computer Science 5, pages 366–377. IEEE Computer Society Press, 1990.

[Tay91] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. Reprinted, 2000.

[Thi97a] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. Also available as technical report ECS-LFCS-97-376.

[Thi97b] Hayo Thielecke. Continuation semantics and self-adjointness. In Proceedings MFPS XIII, volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier, 1997. URL:

        http://www.elsevier.nl/locate/entcs/volume6.html.

[Vic99] Steven Vickers. Topical categories of domains. Mathematical Structures in Computer Science, 9:569–616, 1999.

The papers on abstract Stone duality may be obtained from

                                 www.cs.man.ac.uk/∼pt/ASD

[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300– 366, 2002.

[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[E–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality. Category

Theory and Computer Science, Ottawa, 2002. ENTCS 69.

[E] Paul Taylor, Computably based locally compact spaces. May 2003.

[F] Paul Taylor, Scott domains in abstract Stone duality. March 2002.

[G] Paul Taylor, An elementary theory of the category of locally compact locales. March 2003.

An earlier version of this paper was refereed for and presented at Category Theory 2000, Como, July 2000.