Finite vector-space copowers in a $k$-linear abelian category

Fix the finite basis $(v_1,\dots ,v_n)$ of $V$ and let $A=Y^n$ be the supplied $n$-fold biproduct of $Y$ with injections $i_1,\dots ,i_n$; for $n=0$ this is the empty biproduct, the zero object (Biproduct, Additive category). For each object $Z$ the evaluations $f\mapsto (f(v_1),\dots ,f(v_n))$ and $g\mapsto (g\circ i_1,\dots ,g\circ i_n)$ are bijections ${\mathrm{Hom}}_k(V,\mathcal{C}(Y,Z))\to \mathcal{C}(Y,Z{)}^n$ and $\mathcal{C}(A,Z)\to \mathcal{C}(Y,Z{)}^n$ by [F1] and [F2], so their composite is a bijection ${\eta }_Z:\mathcal{C}(A,Z)⟶{\mathrm{Hom}}_k(V,\mathcal{C}(Y,Z))\mathrm{.}$ For $u:Z\to Z^{\mathrm{\prime }}$ both ${\eta }_{Z^{\mathrm{\prime }}}(u\circ g)$ and the componentwise composite $u\circ {\eta }_Z(g)$ have $j$-th entry $u\circ g\circ i_j$, so $\eta$ is natural in $Z$ (Natural transformation and its components, The hom-bifunctor of a preadditive category takes values in abelian groups); the universal element $u_A={\eta }_A(1_A)$ is the linear map with $u_A(v_j)=i_j$, so $(A,u_A)$ represents the functor $Z\mapsto {\mathrm{Hom}}_k(V,\mathcal{C}(Y,Z))$ (The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding, Natural isomorphism).

Let $(v_1^{\mathrm{\prime }},\dots ,v_n^{\mathrm{\prime }})$ be a second finite basis and write $v_k^{\mathrm{\prime }}={\sum }_j{s}_{jk}{v}_j$ for the invertible scalar matrix $S=(s_{jk})$ (Linear map between vector spaces over the same field). The associated representation is $(A,u_A^{\mathrm{\prime }})$ with $u_A^{\mathrm{\prime }}(v_k^{\mathrm{\prime }})=i_k$; by linearity and [F2] there is a unique endomorphism $\varphi :A\to A$ with $\varphi \circ u_A=u_A^{\mathrm{\prime }}$, its matrix being determined by $S$, and the same construction with the two bases interchanged gives a two-sided inverse, so $\varphi$ is invertible. By [F4] applied to the two universal elements of the functor of step 1.1, $\varphi$ is the unique compatible isomorphism between the two representing objects; hence $V\odot Y$ is determined up to a unique compatible isomorphism and is independent of the chosen basis of $V$.

Let $h:Y\to Y^{\mathrm{\prime }}$ and let $(A^{\mathrm{\prime }},u^{\mathrm{\prime }})$ be the representation of $Z\mapsto {\mathrm{Hom}}_k(V,\mathcal{C}(Y^{\mathrm{\prime }},Z))$ produced by step 1.1, with natural bijections ${\eta }_Z^{\mathrm{\prime }}$. Precomposition with $h$ gives maps $h_{\ast }:\mathcal{C}(Y^{\mathrm{\prime }},Z)\to \mathcal{C}(Y,Z)$, $g\mapsto g\circ h$, componentwise linear, and the composite ${\theta }_Z:=({\eta }_Z{)}^{-1}\circ h_{\ast }\circ {\eta }_Z^{\mathrm{\prime }}$ is a natural transformation $\mathcal{C}(A^{\mathrm{\prime }},-)\Rightarrow \mathcal{C}(A,-)$ (Natural transformation and its components, Covariant functor, identity functor, composite functor, and contravariant functor). By [F3] applied to the objects $A^{\mathrm{\prime }}$ and $A$ there is a unique morphism ${\varphi }_h:A\to A^{\mathrm{\prime }}$ with ${\theta }_Z(f)=f\circ {\varphi }_h$ for every $f:A^{\mathrm{\prime }}\to Z$, and this is the structural morphism $V\odot Y\to V\odot Y^{\mathrm{\prime }}$ induced by the representing property.

Let $\lambda :V\to V^{\mathrm{\prime }}$ be a $k$-linear map. Precomposition gives ${\lambda }^{\ast }:{\mathrm{Hom}}_k(V^{\mathrm{\prime }},\mathcal{C}(Y,Z))\to {\mathrm{Hom}}_k(V,\mathcal{C}(Y,Z))$, $g\mapsto g\circ \lambda$, and the composite $({\eta }_Z^V{)}^{-1}\circ {\lambda }^{\ast }\circ {\eta }_Z^{V^{\mathrm{\prime }}}$ is a natural transformation $\mathcal{C}(A^{V^{\mathrm{\prime }}},-)\Rightarrow \mathcal{C}(A^V,-)$; by [F3] it is induced by a unique morphism $V\odot Y\to V^{\mathrm{\prime }}\odot Y$, the structural morphism in the coefficient variable (k-linear categories and k-linear functors, Linear map between vector spaces over the same field).

For natural transformations $\alpha :\mathcal{C}(A,-)\Rightarrow \mathcal{C}(B,-)$ and $\beta :\mathcal{C}(B,-)\Rightarrow \mathcal{C}(C,-)$, [F3] gives ${\alpha }_c(f)=f\circ E(\alpha )$ and ${\beta }_c(g)=g\circ E(\beta )$, hence $E(\beta \circ \alpha )=E(\alpha )\circ E(\beta )$; identities correspond to identities. Now take the family of representing objects and universal elements in the statement as supplied data. The transformations in steps 2.2 and 2.3 go opposite to the corresponding maps of pairs, and their composites act by $g\mapsto g\circ h\circ h^{\mathrm{\prime }}$ in the object variable and by $f\mapsto f\circ {\lambda }^{\mathrm{\prime }}\circ \lambda$ in the coefficient variable. These operations commute with one another, so their representing morphisms preserve identities and composition and give the asserted functor $(V,Y)\mapsto V\odot Y$. This proves functoriality of the supplied family, without selecting one globally from objectwise existence.

The isomorphism $\mathcal{C}(V\odot Y,Z)\cong {\mathrm{Hom}}_k(V,\mathcal{C}(Y,Z))$ is $k$-linear, since basis evaluation and composition with the biproduct injections are $k$-linear. It is therefore the enriched tensor isomorphism of [F5] over all $k$-vector spaces. A finite-dimensional enriching base is available only when all hom-spaces of $\mathcal{C}$ are finite-dimensional. The objectwise existence and basis comparison require only finite data; functoriality uses the supplied family as in step 3.1.