Re: Generalization of Browder's F.P. Theorem?

Re: Generalization of Browder's F.P. Theorem?

[Carl Futia]

There seems to be some confusion about the theorem Peter McBurney asked about.

The reference he cited was by Felix E. BROWDER (1960) who proved a number of
fixed point results of considerable interest to functional analysts.

The theorem the list seems to be discussing is due to BROUWER (Math. Ann.
69(1910) and 71(1912).

Carl Futia

Re: Generalization of Browder's F.P. Theorem?

[S Vickers]

At 11:19 17/01/03 EST, you wrote:
>There seems to be some confusion about the theorem Peter McBurney asked
about.
>
>The reference he cited was by Felix E. BROWDER (1960) who proved a number of
>fixed point results of considerable interest to functional analysts.
>
>The theorem the list seems to be discussing is due to BROUWER (Math. Ann.
>69(1910) and 71(1912).
>
>Carl Futia

No, there is no confusion. Browder's theorem appears to provide insight
into the constructive content of Brouwer's theorem. Both are being discussed.

Steve Vickers.

Re: Generalization of Browder's F.P. Theorem?

[Andrej Bauer]

Michael Barr <barr@barrs.org> writes:
> For Bishop, a real number is an equivalence class of pairs of
> RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n -
> a_m/b_m| < 1/m + 1/n ...

Actually, Bishop purposely avoids taking a real to be an equivalence
class of sequences, presumably because he does not want to assume the
axiom of countable choice.

A sequence as described above is sometimes called a "fundamental
sequence". Two such sequences x = (a_n/b_n) and y = (c_n/b_n) are
said to "coincide", written x ~ y iff

                   |a_n/b_n - c_m/d_m| < 2/n + 2/m,

where I might have gotten the right-hand side slightly wrong.

Now there are two possibilities:

(1) we say that a real is an equivalence class of fundamental
sequences under the relation ~, or

(2) we say that a real _is_ a fundamental sequence, where two reals
are claimed "equal" if they coincide (the approach taken by Bishop).

The first alternative gives us what is usually called "Cauchy reals".

The difference between the two is apparent when we attempt to show
that every Cauchy sequence of reals has a limit. In the first case we
are given a sequence of equivalence classes of fundamental sequences.
In order to construct a fundamental sequence representing the limit we
need to _choose_ a representative from each equivalence class.

In the second case a Cauchy sequence of reals is a sequence of
fundamental sequences, so no choice is required.

There seems to be an open question in regard to this, advertised by
Alex Simpson and Martin Escardo: find a topos in which Cauchy reals
are not Cauchy complete (i.e., not every Cauchy sequence of reals has
a limit). For extra credit, make it so that the Cauchy completion of
Cauchy reals is strictly smaller than the Dedekind reals.

Has this been advertised on this list already? Or was it the FOM list?

[If anyone replies to this, I suggest you start a new discussion thread.]

Andrej Bauer

Re: Generalization of Browder's F.P. Theorem?

[Michael Barr]

In Errett Bishop's Constructive Analysis (anyone who is interested in
analysis over a topos absolutely must know this book), he proves that for
any continuous endomorphism f of a disk and for every eps > 0, there is a
point x in the disk for which |f(x) - x| < eps.  A couple of points should
be made.  First f has to be constructible and eps has to be provably
positive.  For Bishop, a real number is an equivalence class of pairs of
RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n -
a_m/b_m| < 1/m + 1/n and a function is constructive if it is a machine for
turning one such sequence into another.  To be continuous, it there must
be a function delta(eps) that produces for each eps > 0, a delta(eps) such
that |x - y| < delta(eps) implies that |f(x) - f(y)| < eps.  (In fact,
there is a non-constructive proof that every constructive function is
continuous.)

Bishop then claims, without proof as far as I can see, that there is a
fixed point free endomorphism of the disk.  What this means is that when
you extend this function to all reals, any fixed point is not a
constructible real number.

On Thu, 16 Jan 2003, Steven J Vickers wrote:

>
> I'm intrigued by Peter McBurney's question [below]. It looks rather like a
> question of the constructive content of Brouwer's fixed point theorem.
>
> Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
> topos of sheaves over [0,1], f is just a continuous endomap of S. If
> Brouwer's theorem were constructively true then f would have a fixpoint,
> and that would come out as a continuous section of the projection [0,1]xS
> -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
> g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
> [0,1]} would be as required.
>
> However, the proof of Brouwer that I've seen is not constructive - it goes
> by contradiction. So maybe the requirements on A are a way of getting
> constructive content in Brouwer's result.
>
> What is known constructively about Brouwer's fixed point theorem?
>
> Steve Vickers.
>
> Peter McBurney wrote:
>
> > Hello --
> >
> > Does anyone know of a generalization of Browder's Fixed Point Theorem
> > from R^n to arbitrary topological spaces, or to categories of same?
> >
> > *****************
> >
> > Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
> > subset of R^n, and let
> >
> >         f: [0,1] x S --> S
> >
> > be a continuous function.   Then the set of fixed points
> >
> >          { (x,s) | s = f(x,s), x \in [0,1] and s \in S }
> >
> > contains a connected subset A such that the intersection of A with {0} x
> > S is non-empty and the intersection of A with {1} x S is non-empty.
> >
> > *****************
> >
> > Many thanks,
> >
> > -- Peter McBurney
> > University of Liverpool, UK
>
>
>
>

Re: Generalization of Browder's F.P. Theorem?

[Prof. Peter Johnstone]

On Thu, 16 Jan 2003, Steven J Vickers wrote:

>
> I'm intrigued by Peter McBurney's question [below]. It looks rather like a
> question of the constructive content of Brouwer's fixed point theorem.
>
> Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
> topos of sheaves over [0,1], f is just a continuous endomap of S. If
> Brouwer's theorem were constructively true then f would have a fixpoint,
> and that would come out as a continuous section of the projection [0,1]xS
> -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
> g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
> [0,1]} would be as required.
>
> However, the proof of Brouwer that I've seen is not constructive - it goes
> by contradiction. So maybe the requirements on A are a way of getting
> constructive content in Brouwer's result.
>
> What is known constructively about Brouwer's fixed point theorem?
>
> Steve Vickers.
>
Similar thoughts had occurred to me. Brouwer's theorem is clearly
not constructive, since it doesn't hold (even locally) continuously in
parameters (consider a path in the space of endomaps of [0,1]
passing through the identity, where the fixed point `flips' from
one end of the interval to the other as it does so). However, Browder's
result would seem to suggest that the `locale of fixed points of f'
(that is, the equalizer of f and the identity in the category of
locales) might be consistent (that is, `inhabited') in general,
even though it may not have any points. It's certainly conceivable
that that might be true constructively, though I can't see how to
prove it -- but it isn't the full content of Browder's theorem.

Peter Johnstone

Re: Generalization of Browder's F.P. Theorem?

[Steven J Vickers]

I'm intrigued by Peter McBurney's question [below]. It looks rather like a
question of the constructive content of Brouwer's fixed point theorem.

Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
topos of sheaves over [0,1], f is just a continuous endomap of S. If
Brouwer's theorem were constructively true then f would have a fixpoint,
and that would come out as a continuous section of the projection [0,1]xS
-> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
[0,1]} would be as required.

However, the proof of Brouwer that I've seen is not constructive - it goes
by contradiction. So maybe the requirements on A are a way of getting
constructive content in Brouwer's result.

What is known constructively about Brouwer's fixed point theorem?

Steve Vickers.

Peter McBurney wrote:

> Hello --
>
> Does anyone know of a generalization of Browder's Fixed Point Theorem
> from R^n to arbitrary topological spaces, or to categories of same?
>
> *****************
>
> Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
> subset of R^n, and let
>
>         f: [0,1] x S --> S
>
> be a continuous function.   Then the set of fixed points
>
>          { (x,s) | s = f(x,s), x \in [0,1] and s \in S }
>
> contains a connected subset A such that the intersection of A with {0} x
> S is non-empty and the intersection of A with {1} x S is non-empty.
>
> *****************
>
> Many thanks,
>
> -- Peter McBurney
> University of Liverpool, UK

Generalization of Browder's F.P. Theorem?

[Peter McBurney]

Hello --

Does anyone know of a generalization of Browder's Fixed Point Theorem
from R^n to arbitrary topological spaces, or to categories of same?


*****************

Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
subset of R^n, and let

	f: [0,1] x S --> S

be a continuous function.   Then the set of fixed points

	 { (x,s) | s = f(x,s), x \in [0,1] and s \in S }

contains a connected subset A such that the intersection of A with {0} x
S is non-empty and the intersection of A with {1} x S is non-empty.


*****************

Many thanks,







-- Peter McBurney
University of Liverpool, UK