Polar decompostion should be a diffeomorphism, right? I seem to have gotten stuck in the mud verifying what I thought was going to be a completely straightforward fact. I would appreciate if somebody could help dig me out.  
Inside the $n \times n$ complex matrices $M_n(\mathbb{C})$, let $U, GL, GL_+$ denote, respectively, the unitary matrices, invertible matrices and positive invertible matrices. I was trying to check:

The multiplication map $F : U \times GL_+ \to GL$ sending $(u,p) \mapsto up$ is a diffeomorphism.

Everything here is being viewed as a submanifold of the $2n^2$-dimensional Euclidean space $M_n(\mathbb{C})$. Even though all the scalars here are complex, the objects are being viewed as real manifolds. Some relevant facts:


*

*I calculated the tangent spaces to $U$ and got $T_u(U) = \{ a \in M_n(\mathbb{C}) : u^*a + a^*u = 0 \}.$ That is, $a$ is tangent to $U$ at $u$ if and only if $u^*a$ is anti-self-adjoint.  In particular, $T_1(U)$ is the anti-self-adjoint matrices. 

*$GL_+$ is an open subset of the vector space $SA \subset M_n(\mathbb{C})$ of self-adjoint matrices. So, $T_p(GL_+) = SA$ for all $p \in GL_+$. 

*$GL$ is an open subset of $M_n(\mathbb{C})$ so $T_a(GL) = M_n(\mathbb{C})$ for all $a \in GL$. 


Since $F$ is a bijection (polar decomposition), we will be done if we can show that $F$ has invertible derivative everywhere. The derivatives are given by $DF_{(u,p)} (a,b) = ap + ub$. I figured the easiest thing to do would be to check that this linear map always has zero kernel (since the domain and codomain are manifolds of the same dimension). Look how well this works at the point $(1,1) \in  U \times GL_+$! If $DF_{(1,1)}(a,b) = a+b = 0$ (where $a$ is anti-self-adjoint and $b$ is self-adjoint) then, taking adjoints, we also have $-a + b = 0$. Combining these equations gives $a = b = 0$.
But, I get stuck checking injectivity at other points. Even, say, at $(1,p)$ where $p \in GL_+$. Then, if we take $(a,b) \in T_{(1,p)}(U \times GL_+)$ (i.e. $a^* = -a, b^* = b$) and assume that $DF_{(1,p)}(a,b) = b + ap = 0$, I get stuck doing all sorts of crazy algebra trying to deduce $a=b=0$. 
 A: I think I've proved a lemma which lets me finish this off. [Relevance: Note the squaring map $GL_+ \to GL_+$ is a bijection, since every positive matrix has a unique positive square root. The derivative of the squaring map at $a \in GL_+$ is $b \mapsto ba +ab : SA \to SA$, so the following lemma implies that the square root function is a diffeomorphism of $GL_+$.]

Lemma: If $a \in GL_+$, then $b \mapsto ab + ba : SA \to SA$ is invertible. 

Proof: There exists an orthonormal basis $\xi_1,\ldots,\xi_n$ of $\mathbb{C}^n$ over which $a$ diagonalizes: $a \xi_i = \lambda_i \xi_i$. Moreover, since $a$ is positive and intertible, $\lambda_i > 0$ for all $i$. For each $i,j$ denote by $e_{ij}$ the rank-1 matrix $\xi_i  \xi_j^T$. We have a basis for $SA$ consisting of the $n + 2\binom{n}{2} = n^2$ self-adjoint matrices
\begin{align*}
e_{ii} && 1 \leq i \leq n \\
e_{ij} + e_{ji} && 1 \leq i < j \leq n \\
i(e_{ij} - e_{ji}) && 1 \leq i < j \leq n. 
\end{align*}
Each of these is an eigenvector of $b \mapsto ab + ba$ with corresponding eigenvalues
\begin{align*}
2 \lambda_i && 1 \leq i \leq n \\
\lambda_i + \lambda_j && 1 \leq i < j \leq n \\
\lambda_i + \lambda_j && 1 \leq i < j \leq n. 
\end{align*}
By positivity of the original eigenvalues, none of these new eigenvalues is zero. Hence, $b \mapsto ab + ba : SA \to SA$ is a (diagonalizeable) invertible transformation. QED.
OK, now to finish things off. Suppose that $(u,p) \in U \times GL_+$. Suppose that $(a,b) \in T_{(u,p)}(U \times GL_+)$. That is, $u^*a$ is anti-self-adjoint and $b$ is self-adjoint. Suppose $DF_{(u,p)}(a,b) = ub + ap =0$. Multiplying by $u^*$ on the left and $p^{-1}$ on the right gives $bp^{-1} + u^* a = 0$. Taking the adjoint of the preceding gives $p^{-1} b - u^* a = 0$. Adding the last two equations gives $p^{-1} b + b p^{-1} = 0$. Applying the lemma with $a$ replaced by $p^{-1}$ shows that $b = 0$. It follows easily that $a=0$ as well, so we are done. 
Any feedback/additional perspectives would be welcome. 
