The algebraic closure of the $p$-adic numbers and the axiom of choice Does the algebraic closure of the field $\mathbb{Q}_p$ of $p$-adic numbers exist in ZF without the axiom of choice? If so, how to prove it?
I know that algebraic closures of countable fields can be constructed without the axiom of choice and that it is the uncountable case where choice-free proofs could be a problem. But what about the specific example of $\mathbb{Q}_p$?
 A: The typical construction of $\mathbb{C}_p$ goes through the following steps:

*

*Construct an algebraic closure $\overline{\mathbb{Q}}_p$ of $\mathbb{Q}_p$.

*Note that there is a unique extension of the $p$-adic valuation to $\overline{\mathbb{Q}}_p$, but also that the resulting metric space is incomplete.

*Complete with regards to this metric to get $\mathbb{C}_p$, and show that $\mathbb{C}_p$ is an algebraically closed field.

You are probably worried about the first step, but there's actually also a subtle issue in the third step, which is that the standard definition of the completion of a metric space (i.e., the collection of Cauchy sequences modulo distance $0$) isn't actually 'correct' in situations with very little choice. Specifically, there can be metric spaces $X$ and $Y$ with $X$ dense in $Y$ such that not every element of $Y$ is the limit of a sequence of elements of $X$. So with that in mind, we'll say that a metric space $X$ is complete if the image of any isometric embedding of $X$ into another metric space is closed. $\mathsf{ZF}$ proves that every metric spaces has a unique completion in the typical sense. (There is a way to explicitly construct this completion in terms of 'Cauchy filters' instead of Cauchy sequences.)
To actually answer your question, $\mathsf{ZF}$ does prove that for each prime $p$, there is a valued field $\mathbb{C}_p$ extending $\mathbb{Q}_p$ with the properties that

*

*$\mathbb{C}_p$ is metrically complete and algebraically closed and

*no proper subfield of $\mathbb{C}_p$ containing $\mathbb{Q}_p$ has these properties.

(I don't know whether we can prove that this $\mathbb{C}_p$ is unique in any way.)
Here is a sketch of a terrible proof of this:
Fix a model $V$ of $\mathsf{ZF}$. Let $\mathbb{Q}_p^V$ be $V$'s copy of the $p$-adic numbers. Every model of $\mathsf{ZF}$ has an inner model $L$ of $\mathsf{ZFC}$. Let $\mathbb{Q}_p^L$ be $L$'s copy of the $p$-adic numbers. Since the integers are dense in $\mathbb{Q}_p$, there is a canonical way of thinking of $\mathbb{Q}_p^L$ as a sub-field of $\mathbb{Q}_p^V$. Perform the normal algebraic closure argument inside $L$ to get $\overline{\mathbb{Q}}_p^L$. Let $\mathbb{C}_p^V$ be the metric completion of $\overline{\mathbb{Q}}_p^L$ computed in $V$. Argue that $\mathbb{C}_p^V$ has the required properties: Note that $\mathbb{Q}_p^V$ can be identified with a certain subset of $\mathbb{C}_p^V$. Let $F$ be a proper sub-field of $\mathbb{C}_p^V$ containing $\mathbb{Q}_p^V$ (and therefore also $\mathbb{Q}_p^L$). If $F$ is dense in $\mathbb{C}_p^V$, then $F$ is not metrically complete. If $F$ is not dense in $\mathbb{C}_p^V$, then there is an element $a$ of $\overline{\mathbb{Q}}_p^L$ and a rational $\varepsilon >0$ such that the ball $B_{\leq \varepsilon}(a)$ is disjoint from $F$, but this implies that $F$ is not algebraically closed. Finally we need to check that $\mathbb{C}_p^V$ is algebraically closed. This follows from Hensel's lemma and approximating elements of $\mathbb{Q}_p^V$ with elements of $\mathbb{Q}_p^L$. (Technically we also need to check that $\mathbb{C}_p^V$ has a sensible field structure extending $\overline{\mathbb{Q}}_p^L$, but this is pretty easy.) $\square$
A more honest proof of this would be to build the algebraic closure of some countable dense sub-field of $\mathbb{Q}_p$, such as just the rationals, and then extend the valuation and take the metric completion.
A more difficult question is whether you can always form a spherically complete, algebraically closed field extension of $\mathbb{Q}_p$, since such fields (sometimes denoted $\Omega_p$) are usually constructed using an ultraproduct.
