Matrix associated to a linear transformation Today my linear algebra teacher explained what is the matrix associated to a linear transformation between two finitely generated $\mathbb{K}$-vector spaces.
In particular, if we have $B = \{v_1, \ldots, v_n\}$ basis of $V$ and $C = \{w_1, \ldots, w_m\}$ basis of $W$, then for any linear transformation $f : V \to W$ we have a unique matrix $A = (a_{i j})$ such that $\displaystyle f(v_j) = \sum_{i=1}^m a_{i j} w_i$.
That matrix $A$ was named $M^{B, C}(f)$ and have the following properties:
1) $\forall v \in V . [f(v)]_{C} = M^{B, C}(f) \cdot [v]_B$ (where $[v]_B$ is the vector of the coordinates of $v$ with respect to the basis $B$).
2) $M^{B, D}(g \circ f) = M^{C, D}(g) \cdot M^{B, C}(f)$.
3) $M^{C, B}(f^{-1}) = (M^{B, C}(f))^{-1}$.
4) The matrix of change of basis of the vector space $V$ from the basis $B$ to the basis $C$ is just $M^{B, C}(id)$.
5) If we have a pair of basis of $V$, $B_1$ and $B_2$, and a pair of basis of $W$, $C_1$ and $C_2$, then $M^{C_1, C_2}(id) \cdot M^{B_1, C_1}(f) \cdot M^{B_2, B_1}(id) = M^{B_2, C_2}(f)$.
Now, consider the categories $FVect_\mathbb{K}$ and $Mat_\mathbb{K}$  as here.
Given a function $B$ that associate to any vector space of $FVect$ one of its bases(system of bases?) we have a functor 
$$M_B : FVect_\mathbb{K} \to Mat_\mathbb{K}$$
$$(f : V \to W) \mapsto (M^{B_V, B_W} : \operatorname{dim} V \to \operatorname{dim} W)$$
and given two of these functors we have by (5) the natural transformation
$$
\require{AMScd}
\begin{CD}
n @>{M^{B_V, C_V}(id)}>> n\\
@V{M_B(f)}VV @VV{M_C(f)}V \\
m @>>{M^{B_W, C_W}(id)}> m
\end{CD}
$$
Is all of that right? Can some other interesting things can be said about these functors? Is there any book that talk about vector spaces "in a categoric way"?
 A: As already mentioned, $F$ is an equivalence of categories. But notice that its construction uses the global axiom of choice. We don't really want to choose bases globally. It is more natural to use the functor $\mathsf{Mat} \to \mathsf{FinVect}$ in the other direction which maps $n$ to $K^n$ and a matrix $A : n \to m$ to the linear map $K^n \to K^m$, $x \mapsto Ax$. Then linear algebra facts tell us that this functor is fully faithful and essentially surjective. Using the axiom of global choice, it follows that it is an equivalence.
A variant is the following category $\mathsf{FinVect}'$: Objects are pairs $(V,B)$, where $V$ is a finite-dimensional vector space, and $B$ is a basis of $V$. Morphisms $(V,B) \to (V',B')$ are linear maps $V \to V'$, and the composition is as usual. Then the functor $\mathsf{Mat} \to \mathsf{FinVect}$ factors as $\mathsf{Mat} \to \mathsf{FinVect}' \to \mathsf{FinVect}$, where $\mathsf{Mat} \to \mathsf{FinVect}'$ maps $n$ to $(K^n,(e_1,\dotsc,e_n))$ (the standard basis) and $\mathsf{FinVect}' \to \mathsf{FinVect}$ is the obvious forgetful functor. Now observe that there is a canonical functor $\mathsf{FinVect}' \to \mathsf{Mat}$ which is pseudo-inverse to the given one.
Linear algebra texts usually don't treat category theory, but you might want to read more advanced texts on module categories and then see what happens when the base ring is a field. For example, it is a standard fact that if $R$ is a ring, then $\mathsf{Mod}_R$ is a cocomplete and complete abelian category. This applies in particular to the case of a field. If $R$ is commutative, then one knows that $\mathsf{Mod}_R$ carries a tensor product $\otimes_R$ which makes this category symmetric monoidal. This also applies to the special case that $R$ is a field. See here for a characterization of categories of vector spaces in these terms.
