Constructive predicative Hausdorffification without Choice

124 Views Asked by At

Can the left adjoint to the inclusion functor $i : \mathbf{Haus} \to \mathbf{Top}$ be constructed (1) constructively, (2) predicatively and (3) in ZF?

If all three conditions (i.e., (1), (2) and (3)) are not possible, why and what is the best we can do?

1

There are 1 best solutions below

4
On

I don't know about (1) or (2) but Choice definitely isn't needed. Indeed, I can't think of any construction of the Hausdorffification that uses Choice.

Here's probably the simplest construction. Let $X$ be a topological space and let $\sim$ be the intersection of all equivalence relations on $X$ for which the quotient space is Hausdorff. I then claim that $Y=X/{\sim}$ is Hausdorff. Indeed, let $p:X\to Y$ be the quotient map and suppose $p(x),p(y)\in Y$ are distinct points. Then $x\not\sim y$, so there is some equivalence relation ${\sim'}\supseteq{\sim}$ such that $Z=X/{\sim'}$ is Hausdorff and $x\not\sim'y$. The quotient map $q:X\to Z$ then factors through $p$ via a map $f:Y\to Z$. Since $Z$ is Hausdorff, $q(x)$ and $q(y)$ have disjoint neighborhoods $U$ and $V$ in $Z$. Then $f^{-1}(U)$ and $f^{-1}(V)$ are disjoint neighborhoods of $p(x)$ and $p(y)$ in $Y$.

Thus $Y$ is Hausdorff, and it is now straightforward to show that this operation sending $X$ to $Y$ can be enhanced to a functor that is left adjoint to $i$.