13
$\begingroup$

It's well know that it is surprisingly difficult to prove that $\mathbb{R}^n$ and $\mathbb{R}^m$ are not homeomorphic for $n\neq m$. Commonly proofs go through Brouwer's fixed point theorem, which is 'computably false' for dimensions greater than one: let $K$ denote the computable real numbers. For $n>1$, there are computable functions from $\left( [0,1]\cap K \right)^n$ to itself with no computable fixed point.

That by itself may not seem very bad, since the function may still extend to a continuous function on $[0,1]^n$ and have an incomputable fixed point, but a corollary of this is that there is a computable retraction of $\left( [0,1]\cap K \right)^n$ onto its boundary. Such a function clearly can't be extended to a continuous function on $[0,1]^n$. So we can see that the topological behavior of $K^n$, even when restricted to computable functions, is very different from the topological behavior of $\mathbb{R}^n$.

On the other hand, $K$ is homeomorphic to $\mathbb{Q}$ (although not computably so) and $\mathbb{Q}^n$ is homeomorphic to $\mathbb{Q}^m$ for any $n$ and $m$, so $K^n$ is homeomorphic to $K^m$ for any $n$ and $m$.

So the question is: Is there a computable homeomorphism between $K^n$ and $K^m$ for some $n\neq m$? If there is one I would assume we need $n,m>1$.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ For context, do you know if $\mathbf{Q}$ is computably homeomorphic to $\mathbf{Q}^2$? $\endgroup$
    – YCor
    Commented Jun 20, 2018 at 19:03
  • 3
    $\begingroup$ @YCor Yes, they are; the usual back-and-forth (with requirements) construction of a homeomorphism is totally effective. $\endgroup$
    – Noah Schweber
    Commented Jun 20, 2018 at 19:21
  • 1
    $\begingroup$ There is a proof that $\mathbb R \not\cong \mathbb R^2$. It's effectively the usual one, with the usage of the Constructive Intermediate Value Theorem instead of the classical one $\endgroup$
    – wlad
    Commented Sep 21, 2019 at 16:59
  • $\begingroup$ Of course, this argument implies more generally that $\mathbb R \not \cong \mathbb R^n$ for any $n > 1$ $\endgroup$
    – wlad
    Commented Sep 21, 2019 at 17:03
  • $\begingroup$ See here for the Constructive Intermediate Value Theorem: paultaylor.eu/ASD/lamcra/introivt. The usual proof is an elementary "interval trisection" argument $\endgroup$
    – wlad
    Commented Sep 21, 2019 at 17:07

1 Answer 1

Reset to default
5
$\begingroup$

I believe the full picture to be rather open, but Takayuki Kihara has shown that there is a computable embedding of $K^4$ into $K^3$ in

T. Kihara: The Brouwer invariance theorems in reverse mathematics arXiv 2002.10715

The argument is outlined in the middle of p. 13. It uses Ovrekov's "constructive map of the square into itself, which moves every constructive point", from which it follows that $\mathrm{WKL}$ fails for the computable numbers. Kihara's paper then shows that for any model of $\mathbb{R}$ in which $\mathrm{WKL}$ fails, there is a topological embedding from $\mathbb{R}^m$ into $\mathbb{R}^3$ for any $m$.

Whether we can even have a computable injection of $K^3$ into $K^2$ is listed as an open question here:

http://www.math.mi.i.nagoya-u.ac.jp/~kihara/questions.html

Although I don't have much to go on with, I suspect that asking about mutual embeddability might be the cleaner question here compared to computable homeomorphism.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I hope someone will extract a construction from this paper for the special case of $\mathbb{R}^4$; that would be worth posting as a separate answer. $\endgroup$
    – user44143
    Commented Jul 27, 2020 at 13:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .