categories: Re: Limits

[Andrej Bauer <Andrej.Bauer@andrej.com>]

Tobias Schroeder <tschroed@Mathematik.Uni-Marburg.de> writes:
> So I'd be very grateful for answers to one of the following:
> - Can the limit of a sequence of real numbers be expressed
>   as a categorical limit (of course it can if the sequence is
>   monotone, but what if it is not)?

With a little bit of cheating, you can use domain theory to express
the limit as a sequence as a _colimit_ in a partially ordered set.

Let D be the partial order consisting of all the closed intervals,
including singletons [a,a], ordered by reverse inclusion. We can
embed R into D by mapping it to the maximal elements a |---> [a,a],
and under a suitable topology on D (the Scott topology), this is
a topological embedding--purists may want to throw in R as the
smallest element to obtain an honest continuous domain.

Let x_i be a Cauchy sequence of real numbers. To say that x_i is a
Cauchy sequence is to say that there exist numbers d_i such that

(1) For j >= i, the interval [x_i - d_i, x_i + d_i]
    contains [x_j + d_j, x_j + d_j].

(2) The numbers d_i become arbitrarily small: for every k
    there is i such that for all j >= i, d_i < 1/k.

(Exercise for your students: show that this is equivalent to the usual
definition of Cauchy sequence.)

In terms of the partial order D, (1) says that the intervals
[x_i - d_i, x_i + d_i] form an increasing sequence. Every increasing
sequence in D has a supremum, because an intersection of a nested
sequence of closed intervals is a closed interval, so let

    [u,v] = sup_i [x_i - d_i, x_i + d_i]

By (2), we get that u = v, and we have obtained the limit of the
sequence (x_i) as a supremum. Supremums are the _colimits_ in a
partial order. If you prefer limits, you can stand on your head.

I do not see how to get by without using the _evidence_ that (x_i) is
a Cauchy sequence, i.e., the numbers d_i. This is intuitionistic
mathematics creeping in, which is just as well.

> - Why have people chosen the term "limit" in category theory?
>   (And, by the way, who has defined it first?)

I am way too young to know the answer to this.

Andrej