Unitary group as a regular level set (source code)

= Unitary group as a regular level set
{title2=$\dim_{\mathbb R}U(n)=n^2$}

The smooth map $F(A)=A^*A$ from complex matrices, regarded as a real vector space, to Hermitian matrices has derivative $DF_A(K)=A^*K+K^*A$. At a unitary $A$, taking $K=AH/2$ gives any prescribed Hermitian $H$. Thus $I$ is a <regular value> and $F^{-1}(I)=U(n)$ is a <smooth manifold> of real dimension $n^2$.

// Target: algebra.bigb