In what rigorous sense are Sperner's Lemma and the Brouwer Fixed Point Theorem equivalent?

Question

I understand that one can give a proof of each of these propositions assuming the truth of the other. But this seems a bit squishy to me, since there is a trivial sense in which any two true theorems are equivalent (to any proof of Theorem A, prepend "Assume Theorem B", and vice versa; the objection "But the proof of Theorem A doesn't really use the assumption that Theorem B holds" seems more psychological than mathematical).

One might try to formalize the notion of equivalence by considering the lengths of proofs, saying "There is a derivation of Theorem A from Theorem B that is significantly shorter than any proof of Theorem A from scratch, and vice versa", but this too is squishy, in two distinct ways: the length of a proof depends on the formalization procedure one chooses, and "significantly shorter" is vague. Moreover, it's hard to imagine how one could work with this notion of equivalence, since the totality of all short proofs is going to be hard to get a handle on, for the usual reasons.

Can one find some sort of mathematical context (a topos, perhaps?) in which there is a rigorously defined (and not vacuously true) meaning of the equivalence between Sperner and Brouwer?

(For a recent article that discusses this equivalence and gives pointers to relevant literature, see "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" by Nyman and Su in the April 2013 issue of the American Mathematical Monthly, a version of which is available online at http://willamette.edu/~knyman/papers/Fan_Sperner.pdf .)

See also the related thread Sperner's lemma and Tucker's lemma.

Answer 1

Sperner's lemma is not equivalent to Brouwer's Fixed Point Theorem. All that one can prove directly from Sperner's Lemma is the following weaker statement.

Approximate Fixed Point Theorem. Let $K$ be the standard $n$-dimensional simplex and let $f:K \to K$ be a continuous function. For every $\varepsilon \gt 0$ there is an $x \in K$ such that $|f(x) - x| \leq \varepsilon$.

A compactness argument is then needed to derive the existence of an actual fixed point for $f$.

The analysis is done in §IV.7 of Simpson's Subsystems of Second-Order Arithmetic and the conclusion is that the Brouwer Fixed Point Theorem is equivalent to the Weak König Lemma over the base system RCA₀. On the other hand, since Sperner's Lemma is a finite combinatorial statement, it is provable in RCA₀. The Approximate Fixed Point Theorem is also provable in RCA₀ via Sperner's Lemma. The final compactness argument is however beyond the reach of RCA₀.

Answer 2

The theoretical Computer Science perspective may be useful here. At least, TCS has developed a rigorous and precise sense in which what I'll call "discrete Brouwer" (François' "Approximate Fixed Point Theorem") and Sperner's Lemma are equivalent; and I think it captures the intuition you are seeking in your question. In TCS, we are often interested in the problem you state: understanding when and how $A$ is equivalent to $B$ while avoiding the issue that all true statements imply each other.

The programme is to use reductions to transform one problem into the other, and vice versa. This works on two levels: Algorithmically and logically. Algorithmically, if we can transform an instance of problem $A$ into an instance of problem $B$, such that a solution to $B$ gives back a solution to the original $A$, then we say that $A$ reduces to $B$. If we can also reduce $B$ to $A$, then the problems are equivalent.

Logically, we can interpret the existence of a correct algorithm for $B$ as giving a proof of some theorem (e.g. Brouwer) relating to $B$, and if $A$ reduces to $B$, then this immediately implies a proof of a theorem about $A$. (This is Curry-Howard.) When $A$ and $B$ can be reduced to each other, then a proof of either's associated theorem implies a proof of the other's. Sperner and Brouwer give a beautiful example, which I'll try to sketch as best I can.

---

First, let me define two algorithmic problems.

(Discrete BROUWER) Given $\epsilon$ and a function $f$ that takes coordinates in $[0,1]^2$ and produces coordinates in $[0,1]^2$, output some coordinate $(x,y)$ such that $\|(x,y) - f(x,y)\| \leq \epsilon$.

(SPERNER) Given an integer $n$ and a function $f$ that takes integers $(a,b)$ such that $a+b = n$ (that is, points on a triangulation) and produces a color {red,green,blue} and satisfying the usual Sperner coloring constraints, output a set of three points $((a_1,b_1),(a_2,b_2),(a_3,b_3))$ that (a) is a triangle and (b) is colored with three different colors.

Now, (for this post,) let us just define the discrete Brouwer's Theorem and Sperner's Lemma to be the statements that a solution to the respective problems always exists, for any input.

Now, the problems BROUWER and SPERNER are equivalent in a very precise and rigorous sense: We can reduce each to the other. This means that, given the input to SPERNER, we can show how to transform it into an input to BROUWER. We then can run any algorithm for BROUWER and obtain some output; we then show how to convert this output into an output for the original SPERNER problem. And what we can prove is that, if the algorithm we used for BROUWER is correct, then this algorithm for SPERNER will be correct. Note that we can prove this fact regardless of whether a correct algorithm for Brouwer actually exists or not! Similarly, we can reduce BROUWER to SPERNER by showing how to solve the first by a call to an algorithm for the second.

OK - so far, we have not proven either discrete Brouwer's Theorem or Sperner's Lemma. But now we are in a wonderful spot: If we can only exhibit an algorithm for the SPERNER problem and prove that it is correct, then we will have done both: (1) proven Sperner's Lemma (such a triangle always exists, because we have proven that our algorithm always finds one!); and (2) proven a discrete Brouwer's Theorem (since there is a correct algorithm for SPERNER, we know how to construct an algorithm for BROUWER that always finds an $\epsilon$-fixpoint; so such a fixpoint must always exist).

Similarly, if we can exhibit an algorithm for discrete BROUWER (whose correctness implies the discrete Brouwer theorem), then our reduction above immediately implies an algorithm for solving SPERNER and therefore, Sperner's Lemma.

So, when we algorithmically reduce one problem to the other, we construct a chain of implication: Any algorithm that always solves the other problem implies an algorithm for always solving the first problem. In the case of Brouwer/Sperner, this allows us to show that a solution to the first problem always exists.

My understanding is that the area of homotopy type theory (and perhaps other related fields) are interested in studying the structure of such chains of implications and equivalences, but I know very little about it, so I will stop here. I hope this makes sense; let me know if I can clarify anything!

P.S. A more subtle/further question is whether this really avoids the issue that all true statements imply each other. I don't think it does in a computability sense (?), but it does in a complexity sense: We can only allow polynomial-time reductions between problems. Now, if there is no way to solve either BROUWER or SPERNER in polynomial time, yet we can reduce either to the other in polynomial time, then they must be equivalent in some stronger sense: Our reduction cannot just solve the problem and give some trivial input (since our reduction only runs in polynomial time, which is not enough to solve the problem). So this black-box algorithm we are calling to solve the other problem must be doing the "heavy lifting" in some sense. (Another catch is that we don't know for sure whether BROUWER or SPERNER can be solved in polynomial time, but we mainly conjecture that they cannot.)

Answer 3

Here is another perspective from theoretical computer science. Sperner's theorem represents the complexity class PPAD; This complexity class (described by Christos Papadimitriou) is represented also by finding approximate fix points and several important applications of the fixed-point theorem are known to be PPAD-complete, most famously computing Nash equilibrium of (even 2-players) games. Here is a nice introduction to PPAD by Paul Goldberg, that I found in the post "Brower, Sperner and PPAD$ in this course site of Noam Nisan.

Answer 4

The Brouwer fpp theorem has two components. One is hard-combinatorial, and the other one is soft-analytical (related to compactness). The equivalence in the given case means to neglect the soft part granted that the passage from the hard part to the soft one is simple, preferably trivial.

Actually, the standard connection between Sperner lemma and the Brouwer fpp is not as smooth as it can be. The issue is the choice of the so to speak two stones on each shore--the combinatorial and the analytical--where one can jump easily from one to another.

Let's keep in mind the Sperner lemma used in KKM proof as it appears in Kuratowski's Introduction to the set theory and topology. The easy jump (just a tiny step) from the Sperner lemma to the analysis shore is the theorem about an $n-1$-sphere not being a retract of the respective $n$-ball. Of course there is one more step to get to the actual fpp but--modulo a geometric argument (actually a bit annoying)--it is easily acceptable.

Summary: talk about a so to speak equivalence of Sperner lemma and non-retractability. (Only then, in the second breath, you may mention fpp).