Cauchy completions

Cauchy completions

[Christopher Mulvey]

The construction of the reals as the Cauchy completion of the rationals
was worked out in full and glorious detail in the Montreal spring of
1973. The point is that taking equiconvergence classes of Cauchy
sequences fails to construct the reals in a topos because of the absence
generally of countable choice. Take your favourite example of a topos in
which this fails, and you are most of the way to having your
counter-example.

To obtain the constructive version of the Cauchy reals, coinciding with
the Dedekind reals in any topos with natural number object, you need to
think a little more carefully about you are trying to achieve. The
important thing about a Dedekind real is that there exist rationals that
are arbitrarily close to it. The problem is that of choosing an instance
of a rational at distance < 1/n from the real for each n. If you have
countable choice, then choose away, get a Cauchy sequence, and have an
isomorphism of Cauchy reals with Dedekind reals.

Without countable choice, you still have an inhabited subset of the
rationals consisting of all rationals at a distance of < 1/n from the
Dedekind cut. This gives you a sequence of such subsets - a Cauchy
approximation to the real. The constructive version of the Cauchy reals
is the set of equiconvergence classes of Cauchy approximations on the
rationals. For the details, later extended to the context of seminormed
spaces over the rationals, with the set of rationals as the canonical
example, see papers such as Burden/Mulvey in SLN 753 and my paper Banach
sheaves in JPAA 17, 69-83 (1980).

In the present context, the question is whether you wish to study the
deficiencies of toposes in which countable choice fails, in which case
Cauchy sequences are for you, or whether you want to develop
constructive analysis within a topos, in which case you need to look at
Cauchy approximations instead. Ask yourself, when you take a point in
the closure of a subset, do you get handed a Cauchy sequence converging
to it, or a sequence of possible choices of elements within 1/n of it if
only you had countable choice to choose them. If the former, go for
Cauchy sequences and count your blessings. If the latter, work with
Cauchy approximations, which are every bit as powerful as Cauchy
sequences and with respect to which the reals are Cauchy complete.

Of course, the approach to Banach spaces through completeness defined in
terms of Cauchy approximations acquires collateral justification in
terms of the approaches to Banach sheaves taken by Auspitz and
Banaschewski, to which reference can be found in the papers above. It is
also the approach that allows Gelfand duality to be established
constructively between commutative C*-algebras and compact completely
regular locales in work with Banaschewski and with Vermeulen.

Chris Mulvey.

Re: Cauchy completions

[Alex Simpson]

This is a reply to Chris Mulvey's and Mamuka Jibladze's messages.


Chris Mulvey's message nicely illustrates Martin Escardo's point
that there are different senses in which one might understand
Cauchy completion.

As Chris confirms, it has long been known that, in toposes not
satisfying number-number choice, the Cauchy reals, i.e. the
set of Cauchy sequences (with modulus) quotiented by the obvious
equivalence, are problematic.

Chris takes Cauchy complete to mean complete w.r.t. "Cauchy
approximations" which he defines as:

> Without countable choice, you still have an inhabited subset of the
> rationals consisting of all rationals at a distance of < 1/n from the
> Dedekind cut. This gives you a sequence of such subsets - a Cauchy
> approximation to the real.

As he remarks, it is well known that the Cauchy reals need not be
Cauchy complete w.r.t. Cauchy approximations. Moreover, their "Cauchy
completion" is the object of Dedekind reals. Thus, any of the familiar
toposes in which Cauchy and Dedekind reals differ (e.g. sheaves on R)
provides an example in which the Cauchy reals are not Cauchy complete
w.r.t. Cauchy approximations.

The above story repeats itself exactly if one changes the meaning
of Cauchy completeness to mean completeness w.r.t. a suitable
notion of "Cauchy" filter.

However, Andrej Bauer was referring to Cauchy completeness in
a different sense. A very natural definition of Cauchy
completeness is to merely require completeness w.r.t. Cauchy
sequences (with modulus) of elements. This is weaker than the
definitions above.

The open(?) question Andrej referred to is to find an example of
a topos (if one exists) in which the Cauchy reals are not
themselves Cauchy complete w.r.t. convergent sequences.
For this, one of course requires a topos in which
the Cauchy and Dedekind reals differ (as the latter are
complete). However, the standard examples of such toposes
(e.g. sheaves on R) do not answer the question, for, in them,
the Cauchy reals do turn out to be complete w.r.t. sequences.

One might object to the above question on the grounds that
completeness w.r.t. sequences is not the "correct" notion in a topos.
There is some validity to this. However, the question originally
arose because Martin Escardo and I came up with a definition of an
"interval object" (an object of a category corresponding to the
closed interval [0,1] in much the same way that a "natural numbers
object" corresponds to the natural numbers) that makes sense in
the very general setting of an arbitrary category with finite products.
When interpreted in Set, the interval object is the interval [0,1].
When interpreted in Top it is the interval with Euclidean topology.
When interpreted in an elementary topos, the interval object
turns out to be the interval [0,1] constructed within the "Cauchy
completion w.r.t convergent sequences of the Cauchy reals within the
Dedekind reals", where the quotes are, once again, because the phrase
needs careful interpretation. For mathematical details, see our paper
in LICS 2001 "A Universal Characterization of the Closed Euclidean
Interval".


Our approach apparently has something to say related to Mamuka Jiblaze's
question. For us the interval is defined as an algebra (implementing
an algebraic notion of convexity) freely generated by the object 1+1.
In Top, one can replace 1+1 by Sierpinski space as the generating
object, in which case the interval with the topology of lower
semicontinuity (equivalently the Scott topology) is obtained. Similarly,
in a topos, one might take non-decidable objects (e.g. interesting
"dominances" in the sense of Rosolini) as generating objects.
We have not pursued this latter direction at all, but it might
be interesting to do so.

Alex Simpson

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209