Formal Proof for $\textbf{Vect}_k\cong\textbf{Mat}_k$?

117 Views Asked by At

Where this question came from: I was researching about the graphical languages for monoidal categories involving the category $\textbf{PROP}$ and wanted to see if I could create a graphical language for $\textbf{Vect}_k$ because of $\textbf{Mat}_k$. (probably not the exact reason however this is what I remember)

Let $\textbf{Vect}_k$ be the category of vector spaces for some field $k$ and $\textbf{Mat}_k$ be the category of matrices under the same field $k$.

I know that we can define an equivalence between categories between $\textbf{Vect}_k$ and $\textbf{Mat}_k$ because given vector spaces $V=k^n$ consisting of all $n$-tuples over $k$, and $U=k^m$ consisting of all $m$-tuples over $k$ where $U,V\in\text{Obj}(\textbf{Vect}_k)$, then $\text{Hom}_k(V,U)$ creates the vector space $k^{m\times n}$ representing the set of all $m\times n$ matrices over $k$. Thus showing that $k^{m\times n}\in\text{Obj}(\textbf{Mat}_k)$. If $X=k^{m\times n}$ and $Y=k^{n\times q}$ (set of all $n\times q$ matrices over $k$), then $\text{Hom}(X,Y)=X\otimes Y$ where the tensor product, $\otimes$, is the cross product between the set of matrices $X$ and $Y$. The cross product rules still apply where $\text{Hom}(Y,X)=\emptyset$.

Now lets define the functor $F:\textbf{Vect}_k\to\textbf{Mat}_k$. We have a morphism $f:V\to U$ and the image of $f$ in $\textbf{Mat}_k$, $Ff$, will connect the image of $V$ to the image of $U$. Now I am pretty sure I might be thinking about this wrongly and I hope you could help me with this but I think that $Ff:FV\to FU$ is a morphism from the set of all $m\times1$ matrices to the set if all $1\times n$ matrices. Thus makes $\text{Hom}_{Ff}(FV\to FU)=FV\otimes FU$ which means the cross product between matrices $FV=k^{m\times1}$ and $FU=k^{1\times n}$.

I know this connection however I do not know how to form a formal equivalence proof for $\textbf{Vect}_k\cong\textbf{Mat}_k$. If I could get some help I would greatly appreciate it.

Sources: