I'm trying to understand the proof of Brouwer's theorem form Lawvere and Schanuel's Conceptual Mathematics:
To prove that the non-existence of a retraction implies that every continuous endomap has a fixed point, all we need to do is to assume that there is a continuous endomap of the disk which does not have any fixed point, and to build from it a continuous retraction for the inclusion of the circle into the disk.
This seems to involve unspoken assumptions that I don't know how to justify. If the non-existence of the retraction proves $ \exists x[f(x) = x] $, then I believe that it must also be true that the lack of fixed points $ \forall x[f(x) \neq x] $ implies the existence of a retraction
which shares the same property as the endomap, namely:
$$∀x[(f(x) \neq x)] \to \exists r[r \circ j = 1_C]$$
(Edit note: this expression was originally $∀x[(f(x) \neq x) \to (r(x) \neq x)]$. I mistakenly thought that contradicting $ r(x) \neq x$ was necessary to the argument.)
So my question is twofold:
- How does the lack of a fixed point in the endomap imply (as opposed to simply making possible) the existence of a retraction, $ r \circ j = 1_C $?
- Why is it assumed that the retraction must have properties that
behave as the endomaplead to a contradiction? In other words, it seems like they could be completely independent so that it's both true that $ \forall x[f(x) \neq x] $ and $ r \circ j = 1_C $.
Here's the proof from the book:
So, let $ j: C \to D $ be the inclusion map of the circle into the disk as its boundary, and let's assume that we have an endomap of the disk, $ f: D \to D $, which does not have any fixed point. This means that for every point $x$ in the disk $D$, $f(x) \neq x.$
From this we are going to build a retraction for $j$, i.e. a map $r: D \> \to C$ such that $r \circ j$ is the identity on the circle. The key to the construction is the assumed property of $f$, namely that for every point $x$ in the disk, $f(x)$ is different from $x$. Draw an arrow with its tail at $f(x)$ and its head at $x$. This arrow will 'point to' some point $r(x)$ on the boundary. When $x$ was already a point on the boundary, $r(x)$ is $x$ itself, so that $r$ is a retraction for $j$, i.e. $rj= 1_c$.
(The book doesn't assume any knowledge about topology nor do I know much about it.)