5
$\begingroup$

Apologies if this is too low-level. A related question that I asked on the Math Stack Exchange got no answers after a year, so I thought it might be better to ask this one here.

The standard approach to computable topology is Type Two Effectivity. Its objects of study are represented spaces, which are the $T_0$ subquotients of Baire space $\omega ^ \omega$. The idea is that each point of such a space is represented by names in $\omega ^ \omega$, which can be manipulated computationally. The category of represented spaces is Cartesian closed and so its internal language is simply-typed lambda calculus: we get function types / spaces "for free".

In real-world computation we work with strings of bits rather than natural numbers, i.e. with Cantor space $2 ^ \omega$. Any embedded copy of $\omega ^ \omega$ is neither open (for which we could validate membership of strings) nor closed (for which we could refute it), and cannot be written as the image of such a set since it is not $\sigma$-compact. I am therefore interested in those spaces which can be represented "explicitly", in the following sense:

Consider an open subset $O \subseteq ( 2 ^ \omega ) ^ 2$. It induces a map $f$ from $2 ^ \omega$ to its own space of open sets, where $y \in f ( x ) \Leftrightarrow ( x , y ) \in O$. The open sets in the image of $f$ generate a coarse topology on their union; indeed, there's a computable endofunctor $\mathrm { Gen }$ on open subsets of $(2^\omega)^2$ such that (with a slight abuse of notation) the image of $\mathrm { Gen } ( f )$ is the generated topology. As usual, we'd like to allow multiple names per point and for the space to be $T _ 0$, so take the $T _ 0$ quotient and call $O$ (or $f$) an "explicit representation" of the resulting space.

The category of explicitly represented spaces is not Cartesian closed - it does not even include $\omega ^ \omega$ - but it is still reasonably nice. For example, given any computably enumerable theory $\mathcal { T }$ which is capable of talking about $\omega ^ \omega$, we can restrict $\omega ^ \omega$ to those functions with a bound that $\mathcal { T }$ proves to exist (or proves termination of an algorithm for). We can correspondingly restrict how much of $\omega ^ \omega$ can be used to give names to points, and to construct new represented spaces from old (implicitly, in the growth rates of finite spaces appearing in infinite diagrams). Any space "validated" by $\mathcal { T }$ in this way has an explicit representation, no matter what $\mathcal { T }$ was. And since the space of open sets in $( 2 ^ \omega ) ^ 2$ has an explicit representation, so does the entire category of explicitly represented spaces.

My question then is: have these explicitly represented spaces - or at least the corresponding topological spaces, forgetting the particular representation - been characterized, or discussed at all? What is known about them?

What if we require the image of $f$ to include $2^\omega$ itself? (This excludes e.g. the upper and cofinite topologies on $\omega$, which I know to be non-sober.)

$\endgroup$
2
  • $\begingroup$ It's definitely not low level at all, and an excellent question :-) $\endgroup$
    – David Roberts
    Feb 13, 2021 at 8:29
  • $\begingroup$ Thanks for the feedback! :) $\endgroup$ Feb 14, 2021 at 15:07

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.