Characterization of basis in terms of universal property: axiom of choice I wonder if the proof of the following statement requires the axiom of choice:
(Characterization of basis in terms of universal property) Let $V$ be a vector space, and let $S$ be a non-empty subset of $U$. Show that $S$ is a basis for $V$ if and only if for every vector space $W$ and every function $f : S → W$ , there exists a unique linear transformation $\tilde{f} : V → W$
such that $\tilde{f}(x) = f(x)$ for all $x \in S$.
The proof of the 'if' direction given in this answer certainly uses the axiom of choice, specifically this part:
On the other hand, suppose $E$ is linearly independent but not spanning. $\require{color} \colorbox{yellow}{Extend $E$ to a basis $E'$}$, with $x\in E'\setminus E$.
Any $f:E\to Y$ extends to distinct functions $f_0,f_1:E'\to Y$ defined by $f_0(e)=f_1(e)=f(e)$ for $e\in E$, $f_0(e)=f_1(e)=0$ for $e\in E'\setminus (E\cup\{x\})$, and $f_0(x)=0$, $f_1(x)=1$. Any linear extension of either $f_1$ or of $f_2$ will be a linear extension of $f$. By the forward direction you know that each $f_1$ and $f_2$ have linear extensions. Since $f_1\ne f_2$, these will be distinct linear extensions of $f$.
I don't see any way to circumvent it. However, there is an obvious argument using Yoneda lemma that seemingly does not use the axiom of choice:
Let $F,G: \operatorname{Set}\rightleftarrows \operatorname{Vec}_k$ be the free-forgetful adjunction.The universal property implies that $\operatorname{Set}(S,G(W))\cong \operatorname{Vec}_k(V,W)$ for every vector space $W$ naturally in $W$ (naturally follows from uniqueness of $\tilde{f}$). On the other hand, $\operatorname{Set}(S,G(W))\cong \operatorname{Vec}_k(F(S),W)$. Thus, the representable functors $\operatorname{Vec}_k(V,-)$ and $\operatorname{Vec}_k(F(S),-)$ are naturally isomorphic and hence $V\cong F(S)$ by a corollary of Yoneda lemma and it follows that $S$ is a basis of $V$.
I would like to know whether the proof of the statement requires axiom of choice and if yes, when does the above argument uses the axiom of choice, and if no, how to modify the first proof to get around it.
 A: If $S$ is not a basis, it is either not linearly independent or not spanning.
In the first case, pick some finite counterexample with $n$ vectors, and map them to the standard basis of $F^n$, where $F$ is your field, and everything else goes to $0$. Easily, there is no linear extension of this map, not even to $\operatorname{span}(S)$.
If $S$ is not spanning, simply consider the function into $V/\operatorname{span}(S)$, mapping any element of $S$ to $0$. Since we're not spanning, we can map everything into $0$, or just take the obvious quotient map.
A: The following seems to be a way to complete the "if" direction without extending bases. Suppose $S$ is a set with the given property in terms of linear maps. Let $W=\operatorname{Span(S)}$, a subspace of $V$, then let $p:V\to W$ be the unique map (whose existence is granted by the hypothesis) that extends the inclusion on $S\hookrightarrow W$, and let $\iota:W\hookrightarrow V$ be the inclusion map. Then $\mathbf1_V=\iota\circ p$ since both are linear maps $V\to V$ that coincide on $S$ (I'm using the uniqueness part of the hypothesis here). But then for every $v\in V$ one has $v=\iota(p(v))$ showing that $v\in W$, so that $V=W$.
