localy compact spaces - computably based and over a topos

localy compact spaces - computably based and over a topos

[Taylor Paul]

Drafts of two new papers on Abstract Stone Duality are now available,
and I would very much appreciate your comments about them.

	Computably based locally compact spaces

	An elementary theory of the category of locally compact locales

	http://www.di.unito.it/~pt/ASD

These two papers bring ASD into line with the "official" theory of
locally compact sober spaces and locales, in two completely different
ways.  The ASD "Manifesto" was also revised recently.

	===================================

	Computably based locally compact spaces

The first paper shows that the main version of ASD is equivalent to
the category of "computably based" locally compact locales, and
computably continuous functions.

By a "basis" I mean a family of open subspaces U^n and accompanying
family of compact subspaces K^n, the topological information being
captured by the inclusion relation K^n subset U^m.  For locales the
corresponding idea is the "way below" relation.  The finitary
properties of this are characterised, including in particular the
"Wilker condition" concerning the inclusion of a compact subspace in
the union of two open ones. The motivation of the paper is principally
how to "import" traditional topology into ASD, using the real line as
a running example.

This paper is the expanded version of the one that I presented at
"Category Theory and Computer Science" in Ottawa and the "Domains
Workshop" in Birmingham last August/September.

	===================================

	An elementary theory of the category of locally compact locales

The second paper shows that, when we add an "underlying set" axiom,
the category becomes equivalent to the category of locally compact
locales over any elementary topos.   The usual structure of locale
theory (direct and inverse image maps, Heyting implication, etc)
is DERIVED, in a type-theoretic style.

This is a new characterisation, not only of this category of spaces,
but also of elementary toposes themselves.

(The same technique can be applied to the opposite of the category of
constructively completely distributive lattices, but I haven't filled
in the details of this yet.)

ASD axiomatises its category of spaces directly, not starting from a
category of sets. However, the full subcategory of overt discrete
spaces has emerged to fill this role.  In the traditional situation,
the forgetful functor from spaces to sets has both adjoints (the
discrete and indiscriminate topologies), but of these three functors,
only the leftmost exists in standard ASD.  This paper postulates its
right adjoint, which yields the couniversal overt discrete object
related to any given space.  (Such a thing would be unacceptable in
the main theory, as the equality predicate on the underlying set of
the powerset of N would solve the Halting Problem.)

Whereas the category of sets is an (often unstated) assumption in a
typical mathematical discourse, in this case the topos itself is
constructed from the axioms, viz as this full subcategory.

More significantly, the infinitary joins that are needed to axiomatise
either traditional topology or locale theory are also a consequence of
the axioms, and not a part of them. This is the sense in which the new
axiomatisation deserves to be called elementary.

In fact, the logical power of the theory (powersets in the topos, and
the infinitary joins) arises out of the ``underlying set'' assumption.
We have another example to show that closure of a full subcategory
under (co)limits is a long way from providing an adjoint, and indeed
the existence of the adjoint can be very strong foundational principle
in itself. For example, when well-foundedness is presented in
categorical terms using coalgebras, the extensional ones form a
reflective subcategory, but the axiom of replacement may be needed to
construct the reflection functor. See Exercise 9.62 in my book,
"Practical Foundations of Mathematics".

Paul Taylor
pt@di.unito.it