# Algebraic closure of a field in constructive mathematics

There is a short note by André Joyal called Les théorèmes de Chevalley-Tarski et remarque sur l'algèbre constructive (pp. 256-258). It is claimed there that there is a constructive version of the theorem that every fields embeds in an algebraically closed field in the sense that, for every arithmetic universe $\mathcal{O}$ and every field $k$ in it, there is a conservative extension of $\mathcal{O}$ in which the field $k$ embeds in an algebraically closed field.

The note is very short and there are no actual proofs. So, the question is: did this construction appear in the literature in some form?

[I know that if we put some conditions on the field, then the algebraic closure can be constructed in the same universe. I'm not interested in such theorems. I'm looking for a particular construction that was described in the note.]

• I think the idea is to form the theory of an algebraically closed field containing the original field and then take the classifying arithmetic universe. The problem is partly that Joyal hasn't written up his definition of arithmetic universe, so that we are left to try to work with Maietti's definition. Work of Steve Vickers is definitely relevant here too. – theHigherGeometer Jul 30 '17 at 1:02
• This is worth asking on the categories mailing list, as Joyal is on there. – theHigherGeometer Jul 30 '17 at 1:02
• I believe this was the result that motivated the work on dynamical methods. These are connected to forcing extensions. Here is a recent paper on the topic: A Sheaf Model of the Algebraic Closure Bassel Mannaa Thierry Coquand arxiv.org/pdf/1404.4549 The paper contains a number of historical references. – Bas Spitters Jul 30 '17 at 20:38
• Indeed, Dynamical method in algebra: effective Nullstellensätze Michel Coste Henri Lombardi Marie-Françoise Roy sciencedirect.com/science/article/pii/S0168007201000264 says Cor 2.8 is similar to Joyal's result. – Bas Spitters Jul 30 '17 at 20:46
• References to the works David mentioned: ncatlab.org/nlab/show/arithmetic+pretopos – Bas Spitters Jul 30 '17 at 21:35