Subspaces in Abstract Stone Duality

Paul Taylor

This is part of the core theory of Abstract Stone Duality for locally compact spaces. It was published in Theory and Applications of Categories 10(13) 300–366, July 2002 (BibTeX).



By abstract Stone duality we mean that the topology or contravariant powerset functor, seen as a self-adjoint exponential Σ(−) on some category, is monadic. Using Beck’ theorem, this means that certain equalisers exist and carry the subspace topology. These subspaces are encoded by idempotents that play a role similar to that of nuclei in locale theory.

Paré showed that any elementary topos has this duality, and we prove it intuitionistically for the category of locally compact locales.

The paper is largely concerned with the construction of such a category out of one that merely has powers of some fixed object Σ. It builds on Sober Spaces and Continuations, where the related but weaker notion of abstract sobriety was considered. The construction is done first by formally adjoining certain equalisers that Σ(−) takes to coequalisers, then using Eilenberg–Moore algebras, and finally presented as a lambda calculus similar to the axiom of comprehension in set theory.

The comprehension calculus has a normalisation theorem, by which every type can be embedded as a subspace of a type formed without comprehension, and terms also normalise in a simple way. The symbolic and categorical structures are thereby shown to be equivalent.

Finally, sums and certain quotients are constructed using the comprehension calculus, giving an extensive category.


Postscript: As the Abstract says, the bulk of this paper is concerned with an abstract categorical construction and its re-formulation in a type-theoretic style. This construction is motivated by locally compact spaces, but is not restricted to them, even in a topological setting. It can, for example, be applied to any of various cartesian closed extensions of categories of topological spaces, which are summed up very conveniently in [].

At the time it was written, unfortunately, I lacked the main example that motivates monadicity and Σ-split subspaces. Classically, the map I:Σℝ↣ΣΣℚ×Σℚ defined by

(V⊂ℝ)  open  ↦ {(D,U) ∣ ∃ d∈ D.∃ u∈ U.(d< u)∧[d,u]⊂ V}

in traditional notation, or

φ:Σℝ↦ λδυ.∃ d u. δ d∧υ u∧(d< u)∧∀ x:[d,u].φ x

in our λ-calculus, is Scott-continuous. This map is inter-definable with the universal quantifier ∀:Σ[0,1]→Σ that says that [0,1]⊂ℝ is compact [, ]. The ASD programme therefore provides a formulation of topology and real analysis that is inherently compulable, whilst satisfying this important theorem of mainstream analysis.

For compatibility with the other papers, equality of terms of type Σ is now written ⇔, notwithstanding the fact that no lattice structure is assumed in (most of) this paper.]



Acknowledgements

The original inspiration for this work came during my visit to the Università degli Studi di Genova in March 1993. I would like to thank Martin Hyland, Peter Johnstone, Anders Kock, Fred Linton, Eugenio Moggi, Bob Paré, Andy Pitts, Bob Rosebrugh, Pino Rosolini, Andrea Schalk, Alex Simpson, Thomas Streicher, Steve Vickers, Graham White Todd Wilson and Richard Wood for their valuable comments.



BibTeX entry

   @article{TaylorP:subasd,
      author    = {Taylor, Paul},
      title     = {Subspaces in Abstract {S}tone Duality},
      journal   = {Theory and Applications of Categories},
      publisher = {Mount Allison University},
      year      = 2002, month = {July},
      volume    = 10, number = 13, pages = {300--366},
      url       = {PaulTaylor.EU/ASD/subasd},
      amsclass  = {03E70, 03G30, 06D22, 06E15, 18B05,
                   18B30, 18C20, 18E10, 54C35, 54D45}}

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.




Browse it in HTML


1. Introduction


2. The subspace topology


3. Beck’s theorem


4. Adding Σ-split subspaces


5. Injectives and products in the new category


6. Structure in the new category


7. Algebras


8. Comprehension


9. Normalisation for types


10. Normalisation for terms


11. Sums and quotients


References

This document was translated from LATEX by HEVEA.