If a certain kind of object exists and is unique, can we prove its existence and uniqueness without axiom of choice?

Question

Suppose that using Zorn's lemma, we have proven that an object with some properties exists and then we've proven that such object is unique. Can we always conclude that we can prove the existence (and uniqueness) of the object without using Zorn's lemma (or any other equivalent form of axiom of choice)?

I was studying differentiable manifolds and I arrived to a point where it was proven that any differentiable atlas is contained in some unique maximal differentiable atlas. Then I found out that it can be proven without using axiom of choice. But isn't that because the maximal atlas is unique?

Everywhere I remember that it was necessary to use axiom of choice for proving the existence of some object, it was later proven that such object is not unique and in fact, there are uncountably many of such objects. So I asked the above question, but couldn't find any good answer.

Answer 1

The part about atlases is, as Asaf noted, a duplicate, but let me answer the general question whether uniqueness lets you avoid the axiom of choice. The first counterexample that comes to mind is the smallest ordinal number whose cardinality (i.e., the number of smaller ordinals) equals the cardinality of the real line. The existence of this ordinal is equivalent to the statement that the real line can be well-ordered, so it's provable with the axiom of choice but not without the axiom of choice. Yet the ordinal in question is unique because of "smallest" in its definition.

Answer 2

Not necessarily. You can prove in $\sf ZFC$ that the algebraic closure of $\Bbb Q$ exists and it is unique up to isomorphism. And while you can always prove that $\Bbb Q$ has an algebraic closure, you cannot prove it is unique without appealing to the axiom of choice.

Another example in the same vein is the well-defined notion of a dimension of a vector space. You can prove in $\sf ZFC$ that every vector space has a basis and every two bases have the same cardinality. Proving that every space has a basis implies the axiom of choice (as proven by Andreas Blass in 1984); but even if you know that there is a basis to your space, proving that every two bases have the same cardinality requires you to appeal to the axiom of choice (although it certainly does not imply the axiom of choice in general).

Answer 3

If unique can mean unique up to isomorphism, then no: In ZFC, every field has an algebraic closure, unique up to isomorphism; but there is a model of ZF in which some field has no algebraic closure. Proof of existence of algebraic closures doesn't require full AC — the ultrafilter theorem (aka, dually, the prime ideal theorem) suffices. See for example Can one construct an algebraic closure of fields like $\mathbb{F}_p(T)$ without Zorn's lemma?.