* Re: Generalization of Browder's F.P. Theorem? @ 2003-01-17 16:19 Carl Futia 2003-01-18 12:39 ` S Vickers 0 siblings, 1 reply; 7+ messages in thread From: Carl Futia @ 2003-01-17 16:19 UTC (permalink / raw) To: categories 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Generalization of Browder's F.P. Theorem? 2003-01-17 16:19 Generalization of Browder's F.P. Theorem? Carl Futia @ 2003-01-18 12:39 ` S Vickers 0 siblings, 0 replies; 7+ messages in thread From: S Vickers @ 2003-01-18 12:39 UTC (permalink / raw) To: categories 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Generalization of Browder's F.P. Theorem? @ 2003-01-15 14:00 Peter McBurney 2003-01-16 14:04 ` Steven J Vickers 0 siblings, 1 reply; 7+ messages in thread From: Peter McBurney @ 2003-01-15 14:00 UTC (permalink / raw) To: CATEGORIES LIST 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Generalization of Browder's F.P. Theorem? 2003-01-15 14:00 Peter McBurney @ 2003-01-16 14:04 ` Steven J Vickers 2003-01-16 23:00 ` Prof. Peter Johnstone 2003-01-16 23:05 ` Michael Barr 0 siblings, 2 replies; 7+ messages in thread From: Steven J Vickers @ 2003-01-16 14:04 UTC (permalink / raw) To: CATEGORIES LIST; +Cc: Peter McBurney 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Generalization of Browder's F.P. Theorem? 2003-01-16 14:04 ` Steven J Vickers @ 2003-01-16 23:00 ` Prof. Peter Johnstone 2003-01-16 23:05 ` Michael Barr 1 sibling, 0 replies; 7+ messages in thread From: Prof. Peter Johnstone @ 2003-01-16 23:00 UTC (permalink / raw) To: CATEGORIES LIST 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Generalization of Browder's F.P. Theorem? 2003-01-16 14:04 ` Steven J Vickers 2003-01-16 23:00 ` Prof. Peter Johnstone @ 2003-01-16 23:05 ` Michael Barr 2003-01-21 18:11 ` Andrej Bauer 1 sibling, 1 reply; 7+ messages in thread From: Michael Barr @ 2003-01-16 23:05 UTC (permalink / raw) To: CATEGORIES LIST 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 > > > > ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Generalization of Browder's F.P. Theorem? 2003-01-16 23:05 ` Michael Barr @ 2003-01-21 18:11 ` Andrej Bauer 0 siblings, 0 replies; 7+ messages in thread From: Andrej Bauer @ 2003-01-21 18:11 UTC (permalink / raw) To: CATEGORIES LIST 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 ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2003-01-21 18:11 UTC | newest] Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2003-01-17 16:19 Generalization of Browder's F.P. Theorem? Carl Futia 2003-01-18 12:39 ` S Vickers -- strict thread matches above, loose matches on Subject: below -- 2003-01-15 14:00 Peter McBurney 2003-01-16 14:04 ` Steven J Vickers 2003-01-16 23:00 ` Prof. Peter Johnstone 2003-01-16 23:05 ` Michael Barr 2003-01-21 18:11 ` Andrej Bauer
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).