The dual-basis isomorphism for a finitely generated projective bimodule

($P^{\vee }$ is an $(A,B)$-bimodule.) For $a\in A$ and $\phi \in P^{\vee }$, the prescription $(a\phi )(p):=\phi (pa)$ is additive in $p$ because the right $A$-action and $\phi$ are additive, and it is left $B$-linear because $P$ is a bimodule and $\phi$ is left $B$-linear: $(a\phi )(bp)=\phi ((bp)a)=\phi (b(pa))=b\phi (pa)=b(a\phi )(p)$. For $b\in B$ the prescription $(\phi b)(p):=\phi (p)b$ is additive and left $B$-linear because $(\phi b)(b^{\mathrm{\prime }}p)=\phi (b^{\mathrm{\prime }}p)b=(b^{\mathrm{\prime }}\phi (p))b=b^{\mathrm{\prime }}(\phi (p)b)$. The module laws for $a\mapsto a\phi$ and $b\mapsto \phi b$ follow from the ring laws of $A$ and $B$ and the module laws of $P$, and the two actions commute, $(a\phi )b=a(\phi b)$, because both sides send $p$ to $\phi (pa)b$; hence $P^{\vee }$ is an $(A,B)$-bimodule.

(Existence of a dual basis.) Since $P$ is finitely generated, it has a finite generating set $x_1,\dots ,x_n$ by [F3]; the maps ${\beta }_i:B\to P$, $b\mapsto b{x}_i$, are left $B$-linear, so the universal property of the direct sum $B^n$ gives a unique left $B$-linear $q:B^n\to P$ with $q{\mathrm{ȷ}}_i={\beta }_i$. This $q$ is surjective: every $p\in P$ is a finite $B$-linear combination ${\sum }_i{r}_i{x}_i$ by [F3], and ${\sum }_i{r}_i{x}_i=q({\sum }_i{\mathrm{ȷ}}_i(r_i))$. By [F4] the epimorphism $q$ onto the projective module $P$ has a section $s:P\to B^n$ with $qs=1_P$; write ${\pi }_i:B^n\to B$ for the coordinate projections. Setting $p_i:=x_i$ and ${\phi }_i:={\pi }_i\circ s$ gives left $B$-linear maps ${\phi }_i:P\to B$, and for every $p$ the description of elements of a direct sum [F5] gives $s(p)={\sum }_i{\mathrm{ȷ}}_i({\pi }_i(s(p)))$, so $p=qs(p)={\sum }_i{\pi }_i(s(p))q{\mathrm{ȷ}}_i(1)={\sum }_i{\phi }_i(p)p_i$. Only finitely many objects are selected inside the given finite generating set, so no choice principle is used.

(The evaluation pairing is balanced.) For fixed $y\in Y$ the map $\phi \mapsto (p\mapsto \phi (p)y)$ is additive by [F2], and for fixed $\phi$ the map $y\mapsto (p\mapsto \phi (p)y)$ is additive; the pairing $(\phi ,y)\mapsto (p\mapsto \phi (p)y)$ from $P^{\vee }\times Y$ to ${\mathrm{Hom}}_B(P,Y)$ is therefore additive in each variable. It is $B$-balanced because $(\phi b)(p)y=\phi (p)by=\phi (p)(by)$ for $b\in B$: forming $(\phi b,y)$ and $(\phi ,by)$ gives the same map $P\to Y$.

(The evaluation map exists and is natural.) By the universal property of the tensor product [F6], the balanced pairing of step 1.3 induces a unique group homomorphism $\mathrm{ev}:P^{\vee }{\otimes }_{B}Y\to {\mathrm{Hom}}_B(P,Y)$ with $\mathrm{ev}(\phi \otimes y)=(p\mapsto \phi (p)y)$. For a left $B$-module map $g:Y\to Y^{\mathrm{\prime }}$, the composites ${\mathrm{ev}}_{Y^{\mathrm{\prime }}}\circ (1\otimes g)$ and $g_{\ast }\circ {\mathrm{ev}}_Y$ are group homomorphisms that agree on every elementary tensor $\phi \otimes y$, both sending it to $(p\mapsto \phi (p)g(y))$ by [F8] and [F2]; since the elementary tensors generate the tensor product additively, the two maps are equal, which is naturality in $Y$.

(A candidate inverse from the dual basis.) Fix the dual basis $p_i,{\phi }_i$ of step 1.2 and define $\delta :{\mathrm{Hom}}_B(P,Y)\to P^{\vee }{\otimes }_{B}Y$ by $\delta (h):={\sum }_i{\phi }_i\otimes h(p_i)$; this is a finite sum, and it is additive in $h$ because each evaluation $h\mapsto h(p_i)$ and the tensor product are additive.

(The two composites are identities.) For $h\in {\mathrm{Hom}}_B(P,Y)$, applying $\mathrm{ev}$ to $\delta (h)$ gives the map $p\mapsto {\sum }_i{\phi }_i(p)h(p_i)$, which equals $h(p)$ because $h$ is left $B$-linear and $p={\sum }_i{\phi }_i(p)p_i$; hence $\mathrm{ev}\circ \delta =1$. For an elementary tensor, $\delta (\mathrm{ev}(\phi \otimes y))={\sum }_i{\phi }_i\otimes \phi (p_i)y$. The element ${\sum }_i{\phi }_i\phi (p_i)$ of $P^{\vee }$ equals $\phi$, since for every $p$ one has $({\sum }_i{\phi }_i\phi (p_i))(p)={\sum }_i{\phi }_i(p)\phi (p_i)=\phi ({\sum }_i{\phi }_i(p)p_i)=\phi (p)$ by left $B$-linearity of $\phi$ and the dual-basis formula; hence ${\sum }_i{\phi }_i\otimes \phi (p_i)y=({\sum }_i{\phi }_i\phi (p_i))\otimes y=\phi \otimes y$, so $\delta \circ \mathrm{ev}$ is the identity on elementary tensors and therefore on all of $P^{\vee }{\otimes }_{B}Y$. Thus $\mathrm{ev}$ is a bijection with inverse $\delta$, and it is in particular an isomorphism of abelian groups.

($A$-linearity.) On $P^{\vee }{\otimes }_{B}Y$ the left $A$-action $a(\phi \otimes y)=(a\phi )\otimes y$ is the one of [F7] for the $(A,B)$-bimodule $P^{\vee }$ of step 1.1, and on ${\mathrm{Hom}}_B(P,Y)$ we use $(a\psi )(p)=\psi (pa)$, which is again a left $B$-linear map by the same bimodule computation as in step 1.1. For $a\in A$ and $\phi \otimes y$, $\mathrm{ev}(a(\phi \otimes y))$ sends $p$ to $(a\phi )(p)y=\phi (pa)y$, and $a\mathrm{ev}(\phi \otimes y)$ sends $p$ to $\mathrm{ev}(\phi \otimes y)(pa)=\phi (pa)y$; the two sides agree on elementary tensors and hence everywhere, so $\mathrm{ev}$ is left $A$-linear.

Steps 1.1-1.3 and 2.1 construct the $(A,B)$-bimodule $P^{\vee }$ and the natural evaluation map, steps 2.2 and 3.1 show it is an isomorphism with the stated inverse built from any dual basis, and step 3.2 upgrades it to a left $A$-module isomorphism. Retaining only the group structures, steps 2.1 and 3.1 give the natural isomorphism ${\mathrm{Hom}}_B(P,-)\cong {\mathrm{Hom}}_B(P,B){\otimes }_B-$ of the final sentence: neither the existence of the dual basis nor the two composite computations uses the $A$-action, so for a left $B$-module $P$ finitely generated and projective the result applies with any right $A$-structure on $P$ or with none. The only selections made lie inside the finite data of a generating set and a section, so no choice principle is used.