2 added 523 characters in body

I use the following - hopefully correct - interpretation of the question: We look for examples where AC enables us to construct an object, but AC also proves that this object is unique (up to unique isomorphism if this object is structured).

What about the dimension function $\dim$ which associates to every vector space over $k$ a cardinal number? It is uniquely determined by $\dim(k)=1$ and $\dim(\oplus_i V_i) = \sum_i \dim(V_i)$. Remark that the notion of a cardinal number also makes sense in absence of AC; as well as their sum and therefore this function $\dim$. But existence and uniqueness require AC.

Similarily, the transcendence degree $\mathrm{tr.deg}_k$ associates to every field extension of $k$ a cardinal number. If we vary $k$, these are characterized by (1) $\mathrm{tr.deg}_k(k[t])=1$, (2) $\mathrm{tr.deg}_k(E) = \mathrm{tr.deg}_F(E) \cdot \mathrm{tr.deg}_k(F)$ for $k \subseteq E \subseteq F$, (3) $\mathrm{tr.deg}_k(E)=0$ if $E/k$ is algebraic, (4) $\mathrm{tr.deg}_k(\mathrm{Q}(\bigotimes_i R_i)) = \sum_i \mathrm{tr.deg}_k(\mathrm{Q}(R_i))$ if $R_i/k$ are polynomial rings.

To go into a slightly different and probably more interesting direction: Often AC is needed to show that some object has a certain property, although this object can be defined and understood a priori without AC. There are tons of examples in commutative algebra and algebraic geometry, for example:

Let $k$ be an algebraically closed field, for example $\mathbb{C}$. If $X,Y$ are integral $k$-schemes, then $X \times_k Y$ is again integral. The affine case is: If $A,B$ are $k$-algebras without zero divisors, then the same is true for $A \otimes_k B$. The only proofs I know for this use AC. So in this case, AC also proves the existence of the quotient field of $A \otimes_k B$, which wouldn't make sense if $A \otimes_k B$ wasn't a integral domain.

In linear algebra, you can write down the natural map $i : V \to V^{**}$. It's image $W$ consists precisely of the functionals $V^* \to k$ which are continuous with respect to the weak-*-topology, see here. You have to use AC to show that $i$ is injective and therefore construct the inverse map $W \to V$.

I'm not fully satisfied with these examples. I hope someone else finds more natural examples.

1

I use the following - hopefully correct - interpretation of the question: We look for examples where AC enables us to construct an object, but AC also proves that this object is unique (up to unique isomorphism if this object is structured).

What about the dimension function $\dim$ which associates to every vector space over $k$ a cardinal number? It is uniquely determined by $\dim(k)=1$ and $\dim(\oplus_i V_i) = \sum_i \dim(V_i)$. Remark that the notion of a cardinal number also makes sense in absence of AC; as well as their sum and therefore this function $\dim$. But existence and uniqueness require AC.

Similarily, the transcendence degree $\mathrm{tr.deg}_k$ associates to every field extension of $k$ a cardinal number. If we vary $k$, these are characterized by (1) $\mathrm{tr.deg}_k(k[t])=1$, (2) $\mathrm{tr.deg}_k(E) = \mathrm{tr.deg}_F(E) \cdot \mathrm{tr.deg}_k(F)$ for $k \subseteq E \subseteq F$, (3) $\mathrm{tr.deg}_k(E)=0$ if $E/k$ is algebraic, (4) $\mathrm{tr.deg}_k(\mathrm{Q}(\bigotimes_i R_i)) = \sum_i \mathrm{tr.deg}_k(\mathrm{Q}(R_i))$ if $R_i/k$ are polynomial rings.

To go into a slightly and probably more interesting direction: Often AC is needed to show that some object has a certain property, although this object can be defined and understood a priori without AC. There are tons of examples in commutative algebra and algebraic geometry, for example:

Let $k$ be an algebraically closed field, for example $\mathbb{C}$. If $X,Y$ are integral $k$-schemes, then $X \times_k Y$ is again integral. The affine case is: If $A,B$ are $k$-algebras without zero divisors, then the same is true for $A \otimes_k B$. The only proofs I know for this use AC. So in this case, AC also proves the existence of the quotient field of $A \otimes_k B$, which wouldn't make sense if $A \otimes_k B$ wasn't a integral domain.