Naturality of $\varphi : \textbf{Vct}_K(V(x), w) \xrightarrow{\sim} \textbf{Set}(x, U(w))$ in the variable $x$ (Cats for the Working Mathematician).

Question

Consider the forgetful functor $U : \textbf{Vct}_K \to \textbf{Set}$ and the functor $V : \textbf{Set} \to \textbf{Vct}_K$ that takes an object $x$ in set to the $K$-vector space $V(x)$ with basis $x$ (a type of formal generation) and takes a map $h : x \to x'$ to the $K$-linear map $V(h)(\sum r_i x_i) \ (r_i \in K, x_i \in X) = \sum r_i h(x_i)$.

If $g: x \to U(w)$ is a map of sets, then:

Each function $g: x \to U(w)$ extends to a unique linear transformation $f: V(x) \to w$, given explicitly by $f(\sum r_i x_i) = \sum r_i g(x_i)$. The inverse of $\psi : g \mapsto (f = V(g))$ is $\varphi : f \mapsto f \vert_x$ the restriction of $f$ to the basis set $x$. Thus we have components:

$$ \varphi_{x, w} : \textbf{Vct}_K(V(x), w) \xrightarrow{\sim} \textbf{Set}(x, U(w)) $$

(here $\varphi_{x,w} = \varphi$ from preceeding remark) of a family of bijections between such homsets. These bijections happen to be natural in $x$ and $w$ so we have an isomorphism of bifunctors.

I'm trying to prove naturality of $\varphi$ in the first argument $x$ by showing that the following diagram is commutative for any general $h : x' \to x$ in $\textbf{Set}$ (yes, $x' \to x$ is the correct direction because $x$ is covariantly present in the first (thus, domain-reversing) argument of $\textbf{Vct}_K(V(\cdot), \cdot)$):

$$ \require{AMScd} \begin{CD} \textbf{Vct}_K(V(x), w) @>{\varphi_{x,w}}>> \textbf{Set}(x, U(w))\\ @V{(Vh)^*}VV @VV{h^*}V \\ \textbf{Vct}_K(V(x'), w) @>{\varphi_{x',w}}>> \textbf{Set}(x', U(w)) \end{CD} $$

where $h^*(g) \equiv g \circ h$, $(Vh)^*(g') = g' \circ (Vh)$, and I'm doing this by directly substituting in and expanding the above formulas.

---

We want to show that:

$$ h^* \circ \varphi_{x,w} = \varphi_{x', w} \circ (Vh)^* $$

or equivalently that for any $g:V(x) \to w$ element in the upper left corner of the diagram we have:

$$ [h^* \circ \varphi_{x,w}(g)](y) = [\varphi_{x', w} \circ (Vh)^*(g)](y) $$

for every $y \in V(x)$. Using the definition of $h^*$ etc we have that the above is equivalent showing:

$$ [\varphi_{x,y}(g) \circ h](y) = [\varphi_{x', w} \circ g \circ (Vh)](y) $$

for every $y \in V(x)$. This is where confusion sets in for me.

Answer 1

You're very close; to show this you don't need to refer to explicit elements $y \in V(x')$. To finish this, you need to take take advantage of the universal properties, and interpret what $\varphi_{x,w}$ really does to the morphisms.

To fill in those details you can create a commutative diagram like this: This diagram might help. Here the $i$'s are inclusion morphisms. The last equation you wrote corresponds to the commutativity of the colored-in diagram; see if you can reproduce this diagram by writing explicitly what $\varphi_{x,w}$ does.