I got in an argument once about whether the statement:
"For all fields $F$ the category of finite-dimensional $F$-vector spaces is equivalent to the opposite of the category of $F$-matrices, briefly $\mathsf{FinVect}(F) \simeq \mathsf{Mat}^{\operatorname{op}}(F)$."
is provable in ZF. I argued against it saying something along the lines of "you would need to choose a basis in every vector space".
Is the statement provable in ZF? If not, how does it compare in strength to other consequences of the axiom of choice?
Suppose $F$ is a field such that there is a total order on the underlying set of $F$. Then for any $n$ we have a lexicographical total order on $F^n$.
Suppose we had an equivalence $S: \mathsf{FinVect}(F) \to \mathsf{Mat}^{\operatorname{op}}(F)$.
Let $\mathcal{A}$ be a set of two-element sets.
For any $A\in\mathcal{A}$, $F^A$ is a $2$-dimensional vector space over $F$, as is $F^2$, and so $S(F^A)=S(F^2)$. The identity map $S(F^A)\to S(F^2)$ is $S(\varphi)$ for a unique isomorphism $\varphi:F^A\to F^2$.
Let $\{v_1,v_2\}$ be the natural basis of $F^A$, so there is a natural bijection $A\to\{v_1,v_2\}$, and choose $v_1$ or $v_2$ depending on whether or not $\varphi(v_1)>\varphi(v_2)$ in the lexicographical order.
This gives a choice function for $\mathcal{A}$. But choice for two-element sets is independent of $\text{ZF}$.