Orthogonal complement dimension for a degenerate bilinear form (source code)

= Orthogonal complement dimension for a degenerate bilinear form
{title2=$\dim U+\dim U^\perp=\dim V+\dim(U\cap\ker\Phi)$}

For a <bilinear form> $B$ on a finite-dimensional <vector space> $V$, let $\Phi:V\to V^*$ send $u$ to $B(u,\cdot)$. Under the <bidual evaluation map>, $U^\perp$ is the <annihilator of a vector subspace> $\operatorname{im}(\Phi|_U)$, so $\dim U^\perp=\dim V-\operatorname{rank}(\Phi|_U)$. The <rank-nullity theorem> on $U$ now gives the displayed equality. In particular the sum of dimensions is at least $\dim V$. If $U\cap U^\perp=0$, the <dimension formula for a sum of subspaces> forces $V=U\oplus U^\perp$. The exact formula records the extra dimensions contributed by the left radical $\ker\Phi$, and does not assume an <inner product>.