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