Double commutant theorem for star-algebras (source code)

= Double commutant theorem for star-algebras
{title2=$A^{\prime\prime}=A$}

A unital <subalgebra> $A\subseteq\operatorname{End}(V)$ closed under the <adjoint operator>, on a finite-dimensional real or complex <inner product space>, equals its double <commutant of an operator algebra>. Here is a proof that does not require a classification of <algebras>. For $N=\dim V$, choose a <basis> $(v_1,\ldots,v_N)$ and let $W=\{(av_1,\ldots,av_N):a\in A\}\subseteq V^N$. The diagonal action of $A$ preserves $W$ and $W^\perp$, so the <orthogonal projection> onto $W$ commutes with that action. Each matrix entry of this projection belongs to $A'$. Hence the diagonal action of $b\in A''$ commutes with the projection and preserves $W$. Since $1\in A$, the tuple $(v_1,\ldots,v_N)$ belongs to $W$, and therefore $(bv_1,\ldots,bv_N)=(av_1,\ldots,av_N)$ for one $a\in A$. This implies $b=a$. Without the unital hypothesis the conclusion is $A''=A+\mathbb F1$.