13
$\begingroup$

I'm trying to improve my ability to translate constructive logic into the category theoretical language of topos theory. So far, my understanding of constructive logic has been rather naive. I know that rigorous foundations can be found in HoTT (but not in its book form) and topos theory, but I don't know how to actually use these.

It's known that there exist toposes, like $\operatorname{Sh}(\mathbb C)$, in which the sentence: $$\forall z \in \mathbb C. \exists w \in \mathbb C. w^2 = z$$ is false, where $\mathbb C$ is defined to be the product of the Dedekind reals with themselves. I suspect this is equivalent to saying that the natural projection from ordered pairs of complex numbers to unordered pairs is not surjective. In other words, I suspect that this is equivalent to saying that the natural projection $p:\mathbb C^2 \to \mathbb C^2/\pi$ is not surjective (where $\pi : \mathbb C^2 \to \mathbb C^2$ is the morphism which swaps the two components of its input). This would be strange, because $p$ is supposedly a coequaliser (between $\pi$ and $\operatorname{id}_{\mathbb C^2})$, and a coequalising morphism is always an epimorphism, which should also be a surjection (internal to the topos). How would I express this correctly in categorical language?

The motivation for my interpretation in terms of unordered pairs is that the square roots of a complex number form an unordered pair (conceptually speaking). I suspect that the issue surrounding existence of square roots lies in choosing an element from this unordered pair. But maybe I'm barking up the wrong tree.

$\endgroup$
9
  • 1
    $\begingroup$ Another attempt without talking in general terms about unordered pairs: Understand $S = \{(w,z) \in \mathbb C^2 \mid w^2 = z\}$ to be a pullback. The claim is that the projection $\pi_2 : S \to \mathbb C$ is sometimes not an epimorphism. $\endgroup$
    – wlad
    Oct 26, 2021 at 15:15
  • 1
    $\begingroup$ It would be quite surprising if "every complex number has a square root" and "the quotient map from ordered to unordered pairs of complex numbers is epi" were equivalent: one mentions multiplication and the other one does not. How does your proof of equivalence go? $\endgroup$ Oct 26, 2021 at 17:40
  • 1
    $\begingroup$ @AndrejBauer I didn't say it was true. I said I "intuitively" thought one would be related to the other. An unordered pair in $\mathbb C$ can be represented by the polynomial $f(z) = (z - a)(z-b)$. Let $M(a,b)$ be the matrix whose characteristic polynomial is what I wrote previously. Then $\det(M(a,b)) = ab$, $\operatorname{tr}(M(a,b)) = a + b$, and $M(f(a), f(b)) = f(M(a,b))$ where $f$ is an analytic function on $\mathbb C$. if the matrix $M$ is understood as encoding an unordered pair, the problem boils down to not being able to exhibit an element of this pair. That was my intuition $\endgroup$
    – wlad
    Oct 26, 2021 at 18:08
  • $\begingroup$ @AndrejBauer In this question, I show that an unordered pair in $\mathbb C$ can also be encoded as a normal matrix. This encoding allows one to "map" (in the sense of functional programming) the real part, imaginary part, and magnitude operations over the elements of the pair. It also proves that the claim that a normal matrix has an eigenvalue may be false in some toposes $\endgroup$
    – wlad
    Oct 26, 2021 at 18:11
  • 2
    $\begingroup$ Thanks for insightful comments. This may not be terribly useful for the problem at hand, but Bas Spitter's PhD thesis and some of his subsequent work was about constructive functional analysis – so that's one place to have a look. $\endgroup$ Oct 26, 2021 at 22:18

1 Answer 1

16
$\begingroup$

No the problem isn't quite choosing an element from an unordered pair, even if I agree with you that it somehow feel like it is. The map you are talking about is indeed always an epimorphism.

One way to answer your question is to say that the map $z \mapsto z^2 : \mathbb{C} \to \mathbb{C}$ is not (always) an epimorphism.

Indeed if you look at example you suggest $\operatorname{Sh}(\mathbb{C})$, then $\mathbb{C}$ is the sheaf of continuous complex valued functions and the fonction $z \mapsto z^2$ takes such a function and squares it.

Now one can show that around the point $ 0 \in \mathbb{C}$ the (germ of the) section $z \mapsto z$ cannot be written as the square of the germ of a continus function.

I remember there is a way (or rather several equivalent ways) to define a modified version of $\mathbb{C}^n / S_n$ so that this sheaf is equivalent to the sheaf of unit polynomials of degree $n$ which formalizes the intuition you are talking about in your question, but I can't quite remember how it works. So I prefer not to say too much, but I'm sure someone else can comment or give a reference about this.

E.g. one way this works is that the map from $\mathbb{C}^n \to \mathbb{C}^n$ that sends $n$ complex numbers $(x_1, \dotsc, x_n)$ to the (coefficients of the) unit polynomial $(t-x_1) \dotsb (t-x_n)$ seen as a map of locales, induces an isomorphism of locales $\mathbb{C}^n/S_n \simeq \mathbb{C}^n$. But there are less localic way to say this that might be closer to what you have in mind.

Edit: another approach that I now remember (and I remember reading about it somewhere, maybe someone can say where!). If you endow the set $\mathbb{C}^n/S_n$ with the quotient distance then you can't prove constructively that it is a complete metric space. Here the problem is about chosing an element from an unordered pair, but more precisely with doing it for a whole set of unordered pairs at once, so it require some form of choice. So, because of this, you can consider its metric completion $\overline{\mathbb{C}^n/S_n}$ (in the sense of Cauchy filters) and we can show constructively that the map described above induces a homeomorphism $\overline{\mathbb{C}^n/S_n} \simeq \mathbb{C}^n$. This allows us to show that the axiom of countable choice is enough to show that every complex polynomial admits a root, as countable choice is all you need to prove that $\mathbb{C}^n/S_n$ is complete (though there might be a more direct proof of this).

$\endgroup$
2
  • 2
    $\begingroup$ Among others, a relevant reference is Fred Richman's The Fundamental Theorem of Algebra: a constructive development without choice (link). $\endgroup$ Oct 27, 2021 at 8:08
  • $\begingroup$ Thanks, I think that's exaclty the reference I had in mind ! $\endgroup$ Oct 27, 2021 at 13:41

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.