Freyd's couniversal characterization of [0,1]

Freyd's couniversal characterization of [0,1]

[Martin H. Escardo]

It would be interesting to test Freyd's couniversal characterization
of the unit interval in many other categories.

Here I test it in Top, the category of topological spaces and
continuous maps, and various full subcategories, where one would hope
to get the unit interval with the Euclidean topology.

----------------------------------------------------------------------
Summary of the outcome of some tests:

    (1) In Top, the final coalgebra for Freyd's functor exists. Its
underlying object, however, is an indiscrete space (unsurprisingly).

    (2) In the category of T0 spaces, it doesn't exist.

    (3) In the category of normal spaces it does exist, and, as one
would hope, its underlying object is indeed the unit interval with the
Euclidean topology.

See remark below for weakening normality in (3) as much as possible. 
----------------------------------------------------------------------
Arguments follow. 

We work with the category BiTop of bipointed topological spaces, whose
objects are topological spaces with two distinct distinguished points
and whose morphisms are continuous maps that preserve the two
distinguished points.

Given a bipointed topological space x0,x1:1->X, one constructs a
bipointed topological space FX as in the diagram below, where the
square is a pushout.

               inr           x1
        FX <--------- X <---------- 1
        ^             ^
        |             |
    inl |             | x0
        |             |
        X <---------- 1
        ^       x1
        |
     x0 |
        |
        1.

Thus, FX is the quotient of the coproduct of two copies of X that
identifies two points (x1 of the first copy with x0 of the second).
It is clear how F extends to morphisms producing a functor
BiTop->BiTop.

(1)-----------------------------------------------------------------
Is there a final coalgebra d:I->FI in BiTop? In BiSet, Freyd argued,
one can take I=[0,1] with distinguished points 0 and 1 and structure
map d defined by

       d(x) = inl(2x)    if x<=1/2
              inr(2x-1)  if x>=1/2

Notice that for x=1/2 one gets inl(1)=inr(0), as one should.

[[Incidentally, see M.H. Escardo and Th. Streicher. "Induction
and recursion on the partial real line with applications to Real PCF",
TCS 210(1999) 121-157. There, essentially the same definition gives a
final coalgebra whose inverse is an initial algebra, but the
underlying category is that of continuous Scott domains.]]

By general trivial reasons, the same construction works in BiTop if
one endows X with the indiscrete topology: Uniqueness and existence of
a set-theoretic map follow by Freyd's argument, and any map with
values in an indiscrete space is continuous.

(2)------------------------------------------------------------------
Now consider the category of T0 spaces. For the sake of contradiction,
assume that there is a final coalgebra d:X->FX where X has
distinguished points x0 and x1.

Let S be the space with two points 0 and 1 such that {1} is open but
{0} is not (Sierpinski space). We use the facts that 0<=1 in the
specialization order (every neighbourhood of 0 is also a neighbourhood
of 1) and that continuous maps preserve the specialization order.

Let A be S with distinguished points 0 and 1 (in this order). Then FA
has points 0,1/2,1 with distinguished points 0 and 1. So there is a
unique morphism A->FA. By the alleged finality of d:X->FX there is a
unique homomorphism h:A->X. Since h(0)=x_0 and h(1)=x_1, by continuity
of h we conclude that x0<=x1 in the specialization order. By swapping
the order of the distinguished points of S, we also conclude that
x1<=x0. Thus, x0 and x1 have the same neighbourhoods. By the T0
property, they are equal, which contradicts the definition of a
bipointed topological space.

(3)------------------------------------------------------------------
Now consider the category of normal spaces.  We use Urysohn's Lemma
and Banach's Fixed Point Theorem to show that Freyd's construction
works here if one endows I=[0,1] with the Euclidean topology.

First, d:I->FI as defined by above is clearly a homeomorphism with
inverse c:FI->I given by

       c(inl(x))=x/2
       c(inr(x))=(x+1)/2.

(NB. "d" stands for "destructor" and "c" for "constructor".)

Thus, if D:X->FX is a coalgebra, to say that h:X->I is a coalgebra
homomorphism is the same as saying that

	h = c o Fh o D

We thus consider the obvious functional H:C(X,I)->C(X,I) where C(X,I)
is the set of continuous maps from X to I, namely

	H(h) = c o Fh o D.

(I know, the domain and codomain of H should consist of BiTop
morphisms rather than continuous maps; this (co)restriction will be
performed very shortly).

We endow C(X,I) with the sup-metric, which is well-defined as I is
bounded. It is well-known that this is a complete metric space with
limits of Cauchy sequences computed pointwise. We consider the
subspace B(X,I) of BiTop morphisms.  First, it is non-empty by
Urysohn's Lemma. And this is where the assumption of normality is used
(albeit not in its full strength). Second, it is a complete subspace,
as limits are computed pointwise. Third, H trivially (co)restricts to
a functional H:B(X,I)->B(X,I).

Thus, in order to obtain the desired conclusion, all we have to do is
to show that H:B(X,I)->B(X,I) is contractive.

For every x in X, we have that D(x) is of one of the forms inl(y) or
inr(z), for which we respectively get that, for any h in B(X,I),

	H(h)(x)= c o Fh o inl(y)=h(y)/2		or
	H(h)(x)= c o Fh o inr(z)=(h(z)+1)/2.

Hence in each case we respectively get that

       |H(h)(x)-H(g)(x)|=|h(y)/2-g(y)/2|        =|h(y)-g(y)|/2   or
       |H(h)(x)-H(g)(x)|=|(h(z)+1)/2-(g(z)+1)/2|=|h(z)-g(z)|/2

By definition of the sup-metric, the distance from H(h) to H(g) is the
sup of |H(h)(x)-H(g)(x)| over all x. By the above argument this is
smaller than the sup of |h(t)-g(t)|/2 over all t (because the sup of a
larger set is bigger), which is half the distance from h to
g. Therefore H is contractive. Q.E.D

Remark ---------------------------------------------------------------

Normality in (3) can be generalized to the requirement that for any
two distinct points there is a function into the unit interval that
maps one of the points to 0 and the other to 1 (weak normality). This
is stronger than Hausdorffness and weaker than normality by Urysohn's
Lemma.  But this definition uses the very object that we want to
"construct". Does anyone know a characterization of weak normality
that doesn't refer to real numbers? 

It is easy to see that the assumption that the unit interval with the
Freyd's structure is final in BiC for some subcategory C of Top
implies that all spaces of C are weakly normal.

Thus, the largest full subcategory of Top for which the Euclidean unit
interval with Freyd's structure map is a final coalgebra consists
precisely of the weakly normal spaces.
----------------------------------------------------------------------
Question: What does one get in full subcategories of locales and of
equilogical spaces?
----------------------------------------------------------------------
mailto:mhe@dcs.st-and.ac.uk 
http://www.dcs.st-and.ac.uk/~mhe/
----------------------------------------------------------------------

Re: Freyd's couniversal characterization of [0,1]

[Andrej Bauer]

"Martin H. Escardo" <Martin.H.Escardo@ens.fr> writes:
> It would be interesting to test Freyd's couniversal characterization
> of the unit interval in many other categories.
> 
> Here I test it in Top, the category of topological spaces and
> continuous maps, and various full subcategories, where one would hope
> to get the unit interval with the Euclidean topology.
> 
> ----------------------------------------------------------------------
> Summary of the outcome of some tests:
> 
>     (1) In Top, the final coalgebra for Freyd's functor exists. Its
> underlying object, however, is an indiscrete space (unsurprisingly).
> 
>     (2) In the category of T0 spaces, it doesn't exist.
> 
>     (3) In the category of normal spaces it does exist, and, as one
> would hope, its underlying object is indeed the unit interval with the
> Euclidean topology.
> 
> See remark below for weakening normality in (3) as much as possible. 
> ----------------------------------------------------------------------
> Arguments follow. 
> 
> [text deleted]
>> ----------------------------------------------------------------------
> Question: What does one get in full subcategories of locales and of
> equilogical spaces?

I can answer this for equilogical spaces.

The functor F: Bi[Equ] ---> Bi[Equ] has a final coalgebra. It
is the equilogical space (C, ~) where C is the Cantor space

        C = 2^N = infinite sequences of 0's and 1's

and ~ is the equivalence relation defined by

        a ~ b  iff  r(a) = r(b)

where r: C --> [0,1] is defined by

        r(a) = \sum_{k=0}^\infty a_k / 2^{k+1}

(This equivalence relation can easily be defined without reference to
the closed interval [0,1].) Thus, the final coalgebra is the
_(unsigned) binary digit representation_ of the closed interval [0,1].
The structure map d: (C,~) ---> F(C,~) is induced by the canonical
isomorphism C ---> C + C = 2 x C.

Unfortunately, this closed interval is not what we would hope for.
Ideally, we would want the _signed_ binary digit representation of
the interval [-1,1], i.e., the space ({-1,0,1}^N, :=:) where :=: is
defined by

        a :=: b  iff  s(a) = s(b)

        s(a) = \sum_{k=0}^\infty a_k / 2^{k+1}

We want this because the real numbers object in Equ is the built from
the _signed_ representation of reals.

I do not see how to adapt the construction so that it yields the
signed representation. We would have to "glue" more than just a couple 
of points. But how do we say what should be glued, without reference
to [0,1] or C?

Let me explain briefly why (C, ~) is the final coalgebra. In Equ, in
the pushout

      1 -------> X
      |          |
      |          |
      |          |
      |          |
      V          V
      X -------> FX

the underlying space of FX is |FX| = |X| + |X|. This is a "small" but
crucial difference between Top and Equ. We can first find the final
coalgebra in Top_0 for the functor A --> A + A, which is the Cantor
space C, and then compute the equivalence relation on C. In this case
it is easy to verify that all the continuous maps obtained from the
coalgebraic structure of C actually preserve the equivalence
relations. By the way, the two distinguished points of (C, ~) are
0^\infty and 1^\infty, of course (and it doesn't matter, since C is
homogeneous).

--
Andrej Bauer

Re: Freyd's couniversal characterization of [0,1]

[Martin H. Escardo]

Andrej Bauer writes:
 > I can answer this for equilogical spaces.
 > 
 > The functor F: Bi[Equ] ---> Bi[Equ] has a final coalgebra. It
 > is the equilogical space (C, ~) where C is the Cantor space
 > 
 >         C = 2^N = infinite sequences of 0's and 1's
 > 
 > and ~ is the equivalence relation defined by
 > 
 >         a ~ b  iff  r(a) = r(b)
 > 
 > where r: C --> [0,1] is defined by
 > 
 >         r(a) = \sum_{k=0}^\infty a_k / 2^{k+1}

This is interesting in connection with some previous discussion in
this list on "definability" of the mid-point operation "by
coinduction".

As it is well known, the mid-point operation is not continuously
realizable via binary expansions with the Cantor topology. 

(As Andrej Bauer and other people have mentioned signed-digit binary
expansions in this discussion, let me emphasize that, in contrast to
the above situation, all continuous functions [-1,1]^n->[-1,1] are
continuously realizable via signed-digit binary expansions with the
Cantor topology. Put in another way, the space 3^N = (3^N)^n is
projective over (the regular epimorphism) s:3^N->[-1,1], but the space
2^N is not projective over r:2^N->[0,1].)

Martin Escardo

re: Freyd's couniversal characterization of [0,1]

[Martin H. Escardo]

The following is of course rather unpleasent:

 >     (1) In Top, the final coalgebra for Freyd's functor exists. Its
 > underlying object, however, is an indiscrete space (unsurprisingly).

This can be fixed by choosing a slightly different category of
bipointed objects.

Define a *regularly bipointed object* to be an object X with two
distinguished points x0,x1:1->X such that [x0,x1]:1+1->X is regular
mono. Then the terminal coalgebra for Freyd's functor is 1 iff 1+1=1.

With the restriction to regularly bipointed topological spaces, the
statement (1) becomes false because the two-point discrete space 1+1
is not homeomorphically embeded as a subspace of any indiscrete space.
Hopefully, there isn't a final coalgebra in RegBi(Top), but I don't
see any  if there is,
it cannot be the Euclidean interval.

My previous proof of (2) doesn't work with the proposed modification,
but this should still hold. The argument for (3) is undisturbed.

 >     (2) In the category of T0 spaces, it doesn't exist.
 >
 >     (3) In the category of normal spaces it does exist, and, as one
 > would hope, its underlying object is indeed the unit interval with the
 > Euclidean topology.

Martin Escardo