 Unitary group as a regular level set

The smooth map $F(A)=A^{\ast }A$ from complex matrices, regarded as a real vector space, to Hermitian matrices has derivative $D{F}_A(K)=A^{\ast }K+K^{\ast }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