Locally Compact Spaces in Abstract Stone Duality

Paul Taylor

20 July 2007

Survey papers

Foundations for Computable Topology

PDF (617 kb)
DVI (448 kb)
PostScript (compressed) (375 kb)
A5 PS booklet (compressed) (365 kb)
What are these?
[08 Apr 2009]

This paper surveys the whole of the ASD programme, providing a more detailed guide than this web page to the papers listed below. It also describes the philosophical methodology and the motivations from Marshall Stone's duality between algebra and geometry.

The Dedekind Reals in Abstract Stone Duality

PDF (764 kb)
DVI (550 kb)
PostScript (compressed) (447 kb)
A5 PS booklet (compressed) (425 kb)
What are these?
[03 Jun 2009]

with Andrej Bauer.

§§ 3-5 give the axioms in a "user manual" style, including the monadic lambda-calculus and the definitions of overt, discrete, compact and Hausdorff spaces. This paper also provides the clearest example of the need for the monadic principle.

Introduction to the axiomatisation

The papers below develop the core of ASD, i.e. the theory of computably based locally compact spaces, from four categorical ideas:

the topology on X as the exponential Σ^X, where Σ is the Sierpinski space, and the monadic self-adjunction Σ⁽⁻⁾ −| Σ⁽⁻⁾;
the distributive lattice structure on Σ, and the Euclidean (σ∧Fσ⇔σ∧FT) or Phoa (Fσ⇔F⊥∨σ∧FT) principles that relate the lattice and exponential structures;
recursion and existential quantification over N (the natural numbers); and
Scott continuity (preservation of directed joins).

A fifth idea is not used in the papers listed on this page. This is

the "underlying set axiom", i.e. a right adjoint to the inclusion of the full subcategory of overt discrete spaces.

It explains both the difference in logical strength between the computable theory and one based on set-, type- or topos theory and also the way in which ASD can be extended to and beyond general locales.

Broadly speaking, each of the following papers develops one of the categorical ideas above. It does this

abstractly (relating it to other categorical ideas and examples),
concretely (using the traditional categories of spaces and locales),
by developing a new symbolic language that is equivalent to the categorical one, and
as part of the whole abstract theory of ASD.

These objectives are sometimes in conflict with one another, with the result that it was occasionally not possible to state Theorems in such a clear-cut way as one might like. This was partly due to the need to explore the abstract idea both on its own as widely as possible, and also in the context of the rest of the theory. Secondly, the generality in which each abstract idea is expressed is not the same as that of the corresponding concrete one, so it is not meaningful to assert an equivalence between abstract and concrete sobriety, for example. Finally, it was only at a late stage that I became aware that no further axioms would be required.

The five ideas above are listed in strictly descending order of importance - the fundamental structure is given by the monadic principle, and everything else rides on top on that. In particular, it gives abstract characterisations of certain key ideas in general topology:

sobriety ("half" of monadicity) for N is definition by description;
sobriety for R is Dedekind completeness;
the "other half" of monadicity for R is the Heine-Borel theorem (compactness of [0,1]); and
being a Σ-split subspace of Σ^N captures several different formulations of local compactness.

With the monadic adjunction in place, the Phoa principle is the key to the term calculus, and is what makes the quantifiers, higher order logic, lifting, open-closed duality and everything else work.

I hope that, now that they can see the whole theory more or less in place, readers will appreciate both the expository problems that I faced, and also the solutions that I found for them. Even so, the time is not yet right to reorganise these papers into a book, as that ought instead to present a new theory that would both handle more general spaces and be easier to use than the existing theory of "nuclei".

Please note also that the descriptions of each paper below have been rewritten to tell a continuous story. The original abstracts of course appear on the full papers, but in most cases also in HTML on the journal links.

The papers that develop the core structure

Sober Spaces and Continuations

PDF (533 kb)
DVI (229 kb)
PostScript (compressed) (173 kb)
A5 PS booklet (compressed) (162 kb)
What are these?
[12 Feb 2009]

Theory and Applications of Categories 10:248-299, July 2002.

The idea of a sober space or datatype is that it has exactly the points that are required by its open subspaces or computable predicates.

This can be expressed concretely in terms of filters in the lattice of such subspaces or predicates (§§ A 1 & 5).

The corresponding abstract idea is half of the monadic principle. It says that if Σ^f is invertible then so already is f, or equivalently each object X is a certain equaliser. This is similar to but slightly stronger than the idea of repleteness in synthetic domain theory (§§ A 2-4).

A classical proof is given that locally compact (concretely) sober spaces are abstractly sober (§ A 5).

The same categorical structure was also developed independently by Carsten Führmann, John Power, Peter Selinger and Hayo Thielecke, to study continuation-passing, which is used for compiling New Jersey Standard ML (§§ A 6, 7 & 11).

Symbolically, the simply typed lambda calculus is first restricted to powers of Σ (§ A 2), and then extended with an operator called focus (§ A 8). This has the same beta-rule as Thielecke's force, but may only be applied to an argument that is prime. Primality is defined abstractly as an equation between lambda-terms, but is shown in § G 10 to be equivalent (under Scott continuity) to preservation of the finitary lattice structure. Every term of base type in the calculus with focus is provably equivalent to focus applied to a term of the calculus without it, whilst focus is redundant for higher types.

In the context of the other structure, sobriety of N is equivalent to definition by description, and there is a simple two-way translation between the calculi (§§ A 9-10). This is proved here without using Scott continuity, but with it the equivalence generalises to other overt discrete objects (§ G 10)) . (The corresponding characterisation for R is Dedekind completeness .) It also gives general recursion for total (terminating) programs, and in fact partial ones too (§ D 8) .

The proof of the relationship between focus and recursion in Lemma A 9.6 is wrong, but is corrected in § E 2 .

The paper concludes with a sketch of the translation of the language into (concurrent lambda-) PROLOG (§ A 11).

Subspaces in Abstract Stone Duality

PDF (597 kb)
DVI (320 kb)
PostScript (compressed) (217 kb)
A5 PS booklet (compressed) (206 kb)
What are these?
[12 Feb 2009]

Theory and Applications of Categories 10:300-366, July 2002.

This is the second half of the abstract development of the monadic principle.

The idea that originally inspired ASD (in 1993) is a 1973 theorem of Bob Paré that, in any elementary topos, the contravariant powerset functor Ω⁽⁻⁾ is (self-adjoint and) monadic. This greatly simplified the theory of toposes, since colimits could be derived from limits. A proof is given in this paper that the category of locally compact locales also enjoys the monadic property, with the open set lattice in place of the powerset (§§ B 1-3).

Monads were developed by Fred Linton as an account of infinitary algebra (e.g. in locale theory), and some of the abstract ideas had been investigated by Joachim Lambek

However, Jon Beck's theorem characterising monadic adjunctions turns out to be more relevant in ASD, where it provides certain equalisers (subspaces). These come equipped with the subspace topology; indeed they are Σ-split - there is a canonical way of expending an open subspace of the subspace to one of the ambient space. The clearest example of this was later given by the construction of the Dedekind reals .

Any category of the kind discussed in the previous paper may be completed to one with this monadic property. The construction is done both by formally adjoining Sigma-split equalisers (§§ B 4-6) and then using Eilenberg-Moore algebras (§ B 7).

These subspaces are encoded by idempotents E called nuclei. These are not the same as nuclei in locale theory, but play a similar role. Like primes, they are defined abstractly as an equation between lambda-terms, but are characterised in § G 10 (in the context of the other structure, including Scott continuity) by the equations E(σ∧τ)⇔E(Eσ∧Eτ) and E(σ∨τ)⇔E(Eσ∨Eτ) . Nuclei in locale theory also satisfy id ≤ E, whereas those in (full) ASD are Scott continuous.

A lambda-calculus is given for the subspaces defined by nuclei; this is roughly similar to the axiom of comprehension in set theory (§ B 8). This calculus has a normalisation theorem, by which every type can be embedded as a subspace of a type formed without comprehension (§ B 9), and terms also normalise in a simple way (§ B 10).

Finally, sums and Σ-split quotients are constructed as applications of the comprehension calculus. It is shown that any category with inhabited Σ and the monadic property is extensive; although this is a purely categorical result, the proof relies heavily on the lambda-calculus that is introduced in this paper (§ B 11).

Geometric and Higher Order Logic in terms of ASD

PDF (793 kb)
DVI (382 kb)
PostScript (compressed) (616 kb)
A5 PS booklet (compressed) (333 kb)
What are these?
[11 Apr 2011]

Theory and Applications of Categories 7:284-338, December 2000.

This paper introduces the Euclidean principle, σ∧Fσ⇔σ∧FT. Its two-sided version, Fσ⇔F⊥∨σ∧FT, had arisen as the Phoa principle in synthetic domain theory (§ C 5). (Similar but weaker properties of the subobject classifier in a topos had also been found by Jean Bénabou and Dennis Higgs.) The name was chosen because of the similarity of this equation to Euclid's algorithm for hcf (§ C 4).

Giuseppe Rosolini had defined a dominance as the generalisation of the subobject classifier to other classes of monos, such as open or RE inclusions (§ C 2). The Euclidean principle follows from the uniqueness requirement of any dominance Σ with powers Σ^X. Conversely, the monadic principle supplies the subspaces that any such Euclidean Σ classifies, making it a dominance (§ C 3).

The natural definitions of discrete and Hausdorff spaces correspond to equality and inequality (§ C 6).

The quantifiers considered as adjoints characterise overt and compact spaces. The so-called Frobenius law ∃x.(φ(x)∧σ)⇔(∃x.φ(x))∧σ for the existential quantifier follows from the Euclidean principle, whilst the Beck-Chevalley condition that allows substitution under the quantifier comes automatically from the lambda calculus (§§ C 7 & 8).

The treatment of open and proper maps follows that of André Joyal and Myles Tierney and of Japie Vermeulen respectively, as much as possible, although the word "overt" is new. However, the advantage of ASD is that they are precisely dual.

Some of the arguments about compactness were subsequently popularised by Martín Escardó, though unfortunately without mentioning either the monadic or Euclidean/Phoa principles.

The full subcategory of overt discrete spaces is a pretopos: it has all finite limits, stable disjoint sums (§ C 9) and stable effective quotients of equivalence relations (§ C 10). The latter has always seemed to me to be a miracle, and was the justification for devoting my efforts to ASD full time.

The paper concludes with a converse of Paré's theorem, characterising elementary toposes by means of the monadic and Euclidean properties together with all quantifiers, making no reference to subsets (§ C 11).

Non-Artin Gluing in Recursion Theory and Lifting in ASD

PDF (422 kb)
DVI (166 kb)
PostScript (compressed) (139 kb)
A5 PS booklet (compressed) (128 kb)
What are these?
[12 Feb 2009]

Presented at Category Theory, Como, July 2000; revised June 2001; to be rewritten altogether.

This paper exploits the Phoa Principle as far as possible without using Scott continuity.

The main construction is that of the lift or partial map classifier X_⊥, where the domain of definition of a partial map is open (§ D 2).

The analogous construction in a topos (intuitionistic set theory) involves higher order logic. However, in topology and because of the Phoa principle, it can be seen done as an example of Artin gluing. This recovers the lattice of open subspace of a space as a comma square involving those of an open subspace and its closed complement, together with a map that encodes the way in which these fit together (§ D 1).

Two difficulties arise. First, since ASD is recursive topology, it inherits some of the strange behaviour of recursion theory, and in particular the "open" (RE) subspace of N consisting of codes of terminating programs does not glue to its "closed" (co-RE) complement in anything like the Artin fashion (§ D 4).

Second, the universal properties of gluing and lifting are not the same. Although it is not difficult to derive one from the other in locale theory or using Scott continuity, we want to prove this relationship using finitary structure alone. We find that the modular law is the key idea (§ D 3). There is no claim that topology can be developed using modularity in place of distributivity: the point is that the lattice isomorphism that is required to prove the universal property of lifting from that of gluing is exactly one of the formulations of modularity (§§ D 3 & 6).

The existence of this case of gluing as an object of ASD is proved in §§ D 6-7.

As an application of the lift, general recursion on N (i.e. the search or minimalisation operator) is constructed, without using the fixed points provided by Scott continuity (§ D 8).

The lift is also an example of a partial product. These were introduced by Boris Pasynchov, with the leading example of spheres Sⁿ in Rⁿ⁺¹ and further studied as exponentials in topology by Susan Niefield.

This paper was written as an application of ASD long before it or the community were ready for each other, and so fell foul of the referees. I plan to rewrite it completely when it is clear exactly what development is needed for the theory at this level (i.e. with Phoa, without Scott). For example, it should discuss the similarity between the Phoa principle and Gerhard Gentzen's rules for classical negation. It should also give an account in ASD of the relationship amongst the free lift algebra, co-free lift coalgebra, Scott continuity and other fixed point ideas in (synthetic) domain theory.

Inside every model of ASD lies an Arithmetic Universe

PDF (487 kb)
DVI (195 kb)
PostScript (compressed) (157 kb)
A5 PS booklet (compressed) (146 kb)
What are these?
[12 Feb 2009]

Electronic Notes in Theoretical Computer Science 122, pages 247-296, Elsevier, 2005. An abridged version of this paper had been refereed and accepted for Category Theory and Computer Science 10, Copenhagen, 2004, but was not presented there because I broke my leg the previous week.

This paper exploits Scott continuity (and, of course, recursion and existential quantification over N) to construct the finite powerset (free semilattice) and set of lists (free monoid) on any overt discrete object.

The idea of Arithmetic Universe was introduced by André Joyal in 1973 (but he never published it). It is a pretopos with free monoids, but we have already shown that overt discrete objects form a pretopos.

A Kuratowski-finite subspace of an overt discrete space is overt and compact, so it is represented by its pair ([], < > ) of modal operators, on which it is easy to express the naïve set-theoretic operations (§§ E 3 & 6).

It is much more difficult to define the subspace that provides the free semilattice, and prove its universal property. This accounts for the length of the paper. The subspace is defined by a nucleus, but that is itself defined in a domain-theoretic fashion as a fixed point of a higher order operator (§ E 5).

The fixed point is obtained from an N-indexed least fixed point axiom, as the full Scott-continuity axiom can itself only be stated when we are able to use the free semilattice (§ E 4). The tight correspondence between Kuratowski-finite subspaces and modal pairs also depends on the stronger axiom (§ E 11).

Yet another difficulty arises from the need to use equational hypotheses to reason by induction over N (§ E 2). The upshot of this is that we cannot, after all, axiomatise locally compact spaces alone, but only as part of a larger category that has all finite limits. (This larger category may consist of either general locales or just spatial ones (sober spaces): it is not yet clear which is more appropriate.) The most appropriate way in which to do this is as part of the extended theory.

The free semilattice or finite powerset defines a functor K (§§ E 7 & 10), but in order to prove its universal property (induction and recursion), it is apparently necessary to construct the free monoid or set of lists first (§§ E 8-9).

The finite powerset is considered in a parametric way and as a powerdomain in § E 11.

Computably Based Locally Compact Spaces

PDF (737 kb)
DVI (369 kb)
PostScript (compressed) (244 kb)
A5 PS booklet (compressed) (232 kb)
What are these?
[12 Feb 2009]

Logical Methods in Computer Science, 2 (2006) 1-70; math.GN/0512110.

This paper shows that the full structure, including Scott continuity, completely axiomatises computably based locally compact locales.

A basis is a family of pairs of subspaces: one compact and the other open. The family is indexed by an overt discrete object, wlog N, on which the relevant subspace operations are represented by computable functions. So, for example, a computably continuous function f:R→R is represented by the RE predicate saying whether f[p,q] is contained in (r,s), where p,q,r,s are rational.

The paper has half a dozen sections of introduction before it gets down to business. §§ G 1 & 2 describe how the abstract conditions that will be needed for bases arise from the traditional theories of locally compact spaces and locales respectively, these being subtly different. An important role is played by the inclusion relation of compact subspaces within open ones, which is formulated in locale theory as the way-below relation on a continuous lattice. Achim Jung has discussed similar finitary axioms for strong proximity lattices, notably the Wilker condition for the cover of a compact space by two open ones.

§§ G 3-4 explain the need for a selected basis indexed by an overt discrete object, giving the axioms and relevant results. (It might perhaps have been better to have written another paper about them before launching into this one.)

§ G 5 explores the theory of compact subspaces, both within ASD and using continuous lattices, following Hofmann and Mislove.

§ G 6 characterises local compactness using the basis expansion φx⇔∃n.A_nφ∧βⁿ x and explains how this corresponds to well known ideas for locally compact and compact Hausdorff spaces and locales.

§ G 7 relates the basis expansion to Σ-split subspaces of Σ^N. It also gives the most efficient proof that the category of locally compact locales has the monadic property, and considers the example of the interval domain.

§§ G 8-10 show that every space that is definable in the monadic calculus (§ B 8) has a basis, and derives the characterisations of primes and nuclei.

§ G 11 introduces the abstract way-below relation.

§ G 12 develops the analogue of continuous Scott domains.

§§ G 13-16 show that the finitary axioms are complete, by constructing spaces in the monadic calculus from finitary data about the abstract way-below relation.

Finally, § G 17 shows how this may be used to translate computable bases for classical spaces into objects in the ASD calculus.

This is www.PaulTaylor.EU/ASD/loccpct.php and it was derived from ASD/loccpct.tex which was last modified on 20 February 2011.