Subject: categories: An Abstract Stone Duality

From: Paul Taylor <[email-masked]>
Date: Mon, 4 Jan 1999 21:41:14 GMT

On 29 June 1997, I announced on "categories" my "Euclidean principle"
	f(a) & a = f(true) & a
which holds for any support classifier or dominance Sigma (ie subobject
classifier as in an elementary topos, but for any class of monos, eg open
or RE subsets), where a:X->Sigma and f:X x Sigma -> Sigma.  I gave a 
talk about this at the Category Theory meeting in Vancouver that year.

At the Category Theory meeting in Tours in 1994 I talked about taking
Par\'e's theorem (that the contravariant powerset functor in a topos,
which is self-adjoint, is monadic) as an axiom.  Another category with
this property is the category of locally compact locales, where Sigma is
the Sierpinski space and "powerset" means "lattice of open sets", equipped
with the Scott topology.

This is a way of re-axiomatising general topology without the arbitrary
unions in the traditional definition and in locale theory: the category
of "frames" is to be both dual to the category of "spaces" and algebraic
over it.

I have now written up these ideas as a draft paper entitled
    "An Abstract Stone Duality, I: Geometric and Higher Order Logic"
that you can get via my page in the Hypatia Electronic Library, which is
	http://hypatia.dcs.qmw.ac.uk/author/TaylorP
(I sent copies of an earlier draft to a number of people in November 1998,
but otherwise this is new text: it is not the same as any "notes on SDT"
that you may have got from me over the web in the past.)

After some discussion relating the monadic property to sobriety of spaces
and spatiality of locales, I prove the converse of the basic observation
about the Euclidean principle: if Sigma satisfies it and the adjunction
is monadic then Sigma is the classifier for some class of monos.

It is neither an axiom nor a theorem that the category has all finite limits.
Indeed, the point is that equalisers etc depend on a notion of equality,
which, from a computational point of view, is not as straightforward as
pure mathematicians have traditionally considered it to be.  Some spaces
(datatypes) admit equality in a "positive" way: for example in a group
given by generators and relations, or in a lambda calculus with reduction
rules, we may hope to prove equality of two terms, but not inequality.
On the other hand, we may hope to prove inequality of real numbers but
not equality.  These ideas are formalised by notions of "discrete" and
"Hausdorff" spaces respectively, along with definitions of "open" and
"compact".

We show that the full subcategory of open discrete spaces is a pretopos,
the same being true of the compact Hausdorff spaces, by showing that the
coequaliser is Sigma-split.

The point of Sigma-split co/equalisers is that, being equationally defined,
we might hope to be able to compute with them, possibly using something
like the "continuation-passing style" used in some compilers.

The Euclidean principle and monadicity property are related, respectively,
to the Phoa principle and repleteness in sythetic domain theory.  In that
subject we also need an infinitary axiom that makes all functions Scott
continuous and provides fixed points; this axiom is *not* discussed in
the present paper, largely because this seemed an appropriate criterion
to use to divide up a rambling collection of notes into papers.  The
infinitary axiom and the construction of the "lift" will be considered 
in Part II.

Under the infinitary axiom, open discrete spaces form an arithmetic universe,
ie they admit N-indexed colimits and free algebras, whilst compact Hausdorff
space admit limits and cofree coalgebras.

You might like to consider this paper alongside the recent work of Alex
Simpson and Jaap van Oosten on Synthetic Domain Theory,
	http://www.math.uu.nl/publications/preprints/1080.ps.gz
which is very much concerned with the infinitary axiom.  In particular
Alex is keen to emphasise the additional completeness of the ambient
category that is needed to construct infinitary co/limits and solutions
of domain equations, by comparison with directed joins and fixed points
of functions.  He considers that some attention to the axiom of replacement
is needed here, and I agree with him, though our treatments are different.

My paper is written for a general mathematical audience, and argues its
point of view from a position of extreme Cartesisn doubt.  I feel that
Alex and Jaap's work is very arcane by comparison, as it depends heavily
on Hyland's effective topos.

For my own views on replacement, see the final section of my book,
	Practical Foundations of Mathematics.
I hope to be able to make an announcement about the availability of 
this very soon.