constructive Brouwer fixed point theorem

constructive Brouwer fixed point theorem

[Paul Taylor]

Constructive Brouwer fixed point theorem

I would like some help from a homotopy theorist who is fluent
in the low-level old-fashioned techniques of the subject such
as dividing up polyhedra but who is not frightened by the word
"constructive".

In particular I would like to know whether there is a name or
some theory for a certain kind of higher connectiveness.

Of course I would also like to know whether anyone has already
proved the result that I sketch below, since it does seem rather
a natural one.

The Intermediate Value Theorem and Brouwer's Fixed Point Theorem,
as usually presented, are non-constructive because the proofs
assume that equality in R is decidable, ie you can do one thing
if a=b and another if a<b or a>b.

The counterexample for the IVT is a function that rises to a
"shelf", where it "hovers" for a bit and then rises again,
where the height of the shelf is a value a for which we don't
know whether a=0, a<0 or a>0 and therefore whether the zero is
at the right or left end of the shelf.

There are constructive versions of both results that find places
where the function is zero/fixed within epsilon, without
restricting the (continuous) function.  However, my interest
is in identifying the appropriate restriction on the function
to obtain "exact" results.  Other constructivity questions may
also be raised, such as the use of Dependent Choice and the
"finite open sub-cover" definition of compactness, but I do
not believe that there is any interesting theorem without these.

For the IVT, the condition on the function is that, in any
inhabited open interval, there is some point where it is
nonzero/nonfixed.

The Brouwer fixed point theorem has a counterexample in 2D:
there is a computable endofunction of the square all of whose
fixed points have one or other coordinate non-computable.

Topologically, these fixed points form a rectangular grid,
so that the subspace of non-fixed points is highly disconnected.

Returning to the theorem, there is a well known proof based on
Sperner's Lemma, which is about sub-dividing simplices.

This proof is non-constructive because it assumes at the outset
that the function is non-fixed EVERYWHERE.   However, what is
actually needed to make the proof work is to be able to construct
the sub-division in such a way that the function be non-fixed
on the (n-1)-skeleton.

Therefore the condition on the function that we need to prove
the theorem and avoid the counterexample is a certain higher
connectedness of the (open) subspace of nonfixed points:

Any filled-in (n-1)-simplex such that the function is non-fixed
on its (n-2)-boundary is homotopic (within any neighbourhood)
to a filled-in (n-1)-simplex with the same (n-2)-boundary such
that the function is non-fixed throughout.

This condition is a variant on (n-1)-connectedness, but is not
the same as LOCAL (n-1)-connectedness and I do not know a name
for it.

Recall that a space U is k-connected if for each h <= k, every
continuous map s : S^h -> U is contractible (to a point).

This can be said more abstractly in the form that all of the
homotopy groups pi_n(U) are trivial, but we need a more concrete
form: any hollow k-simplex in U may be filled in within U.

I have a sketch proof of the Brouwer fixed point theorem based
on this hypotheses.   However, a lot of infrastructure about
sub-dividing polyhedra is needed, but this is not my subject
and I am not familiar with it.   Besides, there is no point on
working on this if someone else has already done it.

Also, my real interest is not in the fixed point theorem itself
but in the Sperner proof as an example of the notion of an OVERT
SUBSPACE.

References:

For an introduction to overtness using the IVT as an example,
see my paper
     "A Lambda Calculus for Real Analysis"
     Journal of Logic and Analysis, 2 (2010) 1-115.
     www.paultaylor.eu/ASD/lamcra

This 3-page lecture note by Jacob Fox (formerly of MIT, now
Stanford) contains
- a neat combinatorial proof of Sperner's Lemma and
- its application to the classical Brouwer Fix Point Theorem:
- but not actually the manner of sub-dividing simplices.
math.mit.edu/~fox/MAT307-lecture03.pdf

I don't recall the details of the counterexample in 2D,
which is due to G\"unter Baigger,  but Petrus Potgieter
sketched it for me when I went to Pretoria in 2006 and
in the paper below:

G\"unter Baigger,
Die Nichtkonstruktivit\"at des Brouwerschen Fixpunktsatzes,
Arch. Math. Log., 1985

Petrus Potgieter,
Computable counter-examples to the Brouwer fixed-point theorem,
arxiv.org/abs/0804.3199

Paul Taylor


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]