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.


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: enter image description here 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.

  • 1
    $\begingroup$ Sorry I should clarify that; $i: x \to U(V(x))$ is "universal" in the sense that for any $f: x \to U(W)$ with $W$ a vector space, we have that a unique $g: V(x) \to W$ with the diagram commuting. Here, $\phi$ is a function the other way around: we take a $g: V(x) \to W$ to its unique $\phi_{x, w}(g): x \to U(W)$ such that $U(g) \circ i = \phi_{x, w}(g)$. You might already understand all this so sorry if that's overkill. Anyways, that's what I meant, so apologies if that was confusing. $\endgroup$ – trujello Aug 4 '20 at 20:46
  • 1
    $\begingroup$ Also, I used PGF/TikZ. The manual has a lot of cool stuff to easily make such diagrams! $\endgroup$ – trujello Aug 4 '20 at 20:48
  • 1
    $\begingroup$ So to figure this out, I knew that we needed to figure out what exactly $\phi$ "does." But since I knew $i: x \to U(V(x))$ is universal, I deduced that $\phi$ must send each $g: V(x) \to W$ to the unique $f: x \to U(W)$ such that $U(g) \circ i = f$ (which exist by universality). Thus $\phi$ is defined to go back and forth between $g: V(x) \to W$ and $f: x \to U(W)$ s.t. $U(g) \circ i = f$, which are in unique correspondence by universality. $\endgroup$ – trujello Aug 4 '20 at 20:59
  • 1
    $\begingroup$ And I don't think the code fits in the comments. $\endgroup$ – trujello Aug 4 '20 at 21:01
  • 1
    $\begingroup$ Let us continue this discussion in chat. $\endgroup$ – trujello Aug 4 '20 at 21:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.