Introduction

A locally compact space is one in which there is a good interaction of open and compact subspaces. In this paper we shall show how this interaction can be captured abstractly, establishing an equivalence with a new recursive account of topology.

We shall consider the following formulations of local compactness:

1. open and compact subspaces in a traditional sober topological space (Section 1);
2. disjoint open subspaces in a compact Hausdorff (regular) space (Example 6.11); and
3. the way-below relation ≪ in a continuous distributive lattice (Section 2).

In the categories of locally compact sober spaces and locales, the topology (lattice of open subspaces) of X, considered as another space or locale equipped with the Scott topology, is the exponential Σ^X, where Σ is the Sierpiński space. We shall show how the three classical formulations above give rise to the following abstract structure in this category:

1. families of terms βⁿ:Σ^X and A_n:Σ^ΣX with a basis expansion (Section 6)

   φ x  ⇔  ∃ n.Anφ∧ βn x;

2. a Σ-split inclusion i:X↣Σ^N and I:Σ^X◁Σ^ΣN with Σⁱ· I=id_Σ^X (Section 7);
3. an idempotent E≡ I·Σⁱ on Σ^ΣN (Section 10);
4. an abstract way-below relation n≺≺ m≡ A_nβ^m on N (Section 11); and
5. an Eilenberg–Moore algebra for the monad arising from the adjunction Σ⁽⁻⁾⊣Σ⁽⁻⁾ [B].

We will give complete axiomatisations of each of these structures, and define the translations amongst them, doing this in a new λ-calculus (Abstract Stone Duality). We consider several special cases, in particular the real line, the interval domain (Definition 7.10), continuous dcpos and various kinds of domains (Section 12).

It may help you to find your way around this lengthy paper if I explain that Section 6 was the first to be written. It shows how the classical notions of locally compact space and locale can be expressed in a λ-calculus.

However, the present paper was the first to put this calculus to work to do topology. The previous ones [A, B, C] had examined components of the theory as abstract categorical ideas, without being aware of how many (in fact, few) more such components would be needed to build a logically complete account of topology. Sections 3–4 and 7–10 discuss the way in which these components go together to make a viable theory. This discussion has, in fact, spilled over into several additional papers, in particular [E, H]. If you would prefer to read a dry summary of the axioms in a “user manual” style, please see [I].

Once all this structure is in place, Section 11 begins to take it apart again, characterising the finitary properties of the way below relation in an abstract way. This corresponds to the concrete treatment in Sections 1 and 2. Sections 13–16 construct an object of the ASD calculus from any such abstract relation (with a “practice run” for domains in Section 12) and the final section completes the circle with the traditional theory.