Is it valid to make an admission of a topological space by a “partial quotient map”?

Question

It is well-known that the Sierpiński space, $\{F,T\}$ endowed with topology $\{\emptyset, \{F\},\{F,T\}\}$, is admissible. I tried to implement it in Haskell.

First I implement $\mathbb{N}$ (including zero; some topologists might prefer denoting it by $S_\omega$) by Peano definition:

data Peano = Zero | Succ Peano deriving (Eq, Ord)

This encodes $\mathbb{N}$, but there is one additional value lurking behind: fix Succ. I denote it by $\omega$, and I denote $\mathbb{N} \cup \{\omega\}$ by $\overline{S_\omega}$. We observe that $\overline{S_\omega}$ is in order topology.

I abuse this fact and implement the Sierpiński space by taking a quotient space. The quotient map $q$ is:

$$ q(o) = \begin{cases} F & \text{if } o < \omega \\ T & \text{o.w.} \end{cases} $$

In Haskell, This can be realized by:

newtype Sierpinski = Sierpinski Peano

instance Eq Sierpinski where
    Sierpinski m == Sierpinski n = let
        q m = case m of
            Zero   -> False
            Succ n -> q n
        in q m == q n

But to think about it, q doesn't halt on $\omega$. In other words, q is partial, and doesn't match $q$. Is this really a valid implementation of the Sierpiński space?

Answer 1

When we implement a space we do not actually implement the space itself, but rather a representation of it. That is, an implementation of $X$ consists of a datatype $T$ and a partial surjection $\delta : T \to X$, as in Type Two Effectivity. When $\delta(p) = x$ we say that the datatype value $p \in T$ represents or realizes the point $x \in X$. Cruicially, there may be many values that represent the same point. Only $T$ exists in the computer, $X$ and $\delta$ are mathematical objects. A particularly well-behaved kind of representation is an admissible one, as you mention.

In your case, you correctly implemented an admissible representation of the Sierpinski space: $X$ is the Sierpinski space, $T$ is Sierpinski, and the surjection $\delta$ maps $\omega$ to $\bot$ and $\mathtt{Succ}^n \,\mathtt{Zero}$ to $\top$. There is no need for further quotienting.

The attempt to define == on Sierpinski is not about quotienting, but rather trying to define the characteristic map $\mathrm{eq} : X \to \{0,1\}$ of equality as a map into Booleans, which is only possible when the space is discrete. You discovered that the Sierpinski space is not discrete.

If we have a representation $\delta : T \to X$ then we can form the representation of a quotient $Y = X/{\sim}$ as $\delta' : T \to Y$ where $\delta'(p) = [\delta(p)]_{\sim}$. That is, quotienting affects the map but not the datatype.

Answer 2

Maybe? It depends on your definition of a quotient space. I would say no based on context I think? This is not an over approximation but it is a correct under approximation, albeit not a very useful under approximation. There is a sense in which you $q$ implementation is the best computable approximation of that function that it is the "greatest" computable function consistent with the corresponding classical function.

Domain theoretically, which I claim is the correct tool to use to answer this question, $q(\omega) \not= T$ but instead $q(\omega) = \bot$.

Further, keep in mind that actually Peano has a whole host of other values you didn't account for from a domain theoretical perspective such as $\bot$, $Succ(\bot), Succ(Succ(\bot))$, etc...

So anytime we try to implement a topology in Haskell like this what we're really trying to do is use the actual topology we get from the Haskell values to implement a subspace topology or some kind of embedding. This is known as an over approximation. So for instance we say we implement the natural numbers with the discrete topology using the Peano definition you gave above but we also claim this same type implements other richer topologies like the topology induced by the actual domain for that type or the extended natural numbers as you pointed them out. (P.S. using strictness annotations you can restrict some of these values to get closer to discrete topologies). Sometimes however we just want to implement all of the things we can implement and just accept we can't represent all the classical objects. We do this with the exact reals for instance which are the best computable approximation of the classical reals. This is an example of under approximation.

With quotient spaces things get even more tricky in what hoops we have to jump though to say we've implemented such a space. Mathematically you can quotient by any equivalence relation but with a computer we're generally limited to working only with the decidable equivalence relations. In domain theoretical language that means the equivalence relation must be a continuous function. Another way to implement an equivalence relation is to define a mapping to canonical members which is really what you've done here and you've defined the induced equivalence relation from it. But again you can only define the best computable approximation of the needed mapping here. The issue is that the actual function you need is not continuous/computable.

So we have to make a choice, what counts as a valid approximation? Well the reason we want to call this a quotient space is so that we can think of it as one and apply the theorems and reasoning that come along with thinking about this as a quotient space right? The only way the classical theorems about quotient spaces go though when talking about computable approximations is if we restrict ourselves to decidable/continuous equivalence relations (or equivalently canonicalization maps).

But you could say "well I only really care about the parts that are possible to compute". It turns out this is actually pretty useful sometimes. When working with such approximations as in the above any theorem you use from classical topology that goes wrong will cause an infinite loop but it won't result in your program outputting an incorrect result despite your correct classical proof! So if infinite loops are acceptable behavior in the cases that you can't compute something this is totally acceptable. One paper that springs to mind that does such a thing is A Simple Differentiable Programming Language where they give themselves an out anywhere a discontinuity is hit. For that use case this is a good enough approximation, for others its not.

So the thing to keep in mind is that with computers we're almost always approximating more exotic mathematical structures unless you really are trying to work with a domain in which case that's exactly what Haskell does. The question is then how good of an approximation is acceptable? Do you need an over approximation or is an under approximation good enough?