The complex Grassmann polar map is a first-order retraction

The Gram matrix $C(X,\eta )=I+{\eta }^{\ast }\eta$ is Hermitian positive definite by [F1]. Its realification $\rho (C)$ is real symmetric because $\rho (C{)}^{\mathsf{T}}=\rho (C^{\ast })=\rho (C)$, and positive definite because, for $z=x+iy$, $(x,y{)}^{\mathsf{T}}\rho (C)(x,y)=z^{\ast }Cz>0$. The matrix $\rho (C^{1\mathrm{/}2})$ is real symmetric by the same transpose identity, squares to $\rho (C)$ by [F5], and is positive definite by the same quadratic-form identity. Uniqueness of the positive square root and [F2] therefore make $C^{1\mathrm{/}2}$ smooth in real coordinates. It stays invertible, so [F5] applied to its realification makes its inverse smooth for every finite $k$, and that inverse is the realification of $C^{-1\mathrm{/}2}$. The frame formula and its range are smooth.

Fix horizontal $\eta$ and set $Y(t)=(X+t\eta )(I+t^2{\eta }^{\ast }\eta {)}^{-1\mathrm{/}2}$. The Gram factor has value $I$ at zero and derivative zero there because its argument is $I+t^2{\eta }^{\ast }\eta$ and the inverse-root map is smooth by [F2] and [F5]. The product rule gives $Y(0)=X$ and $Y^{\mathrm{\prime }}(0)=\eta$. By [F3], this is precisely identity on the quotient tangent.

By [F4], the unitary-equivariant frame formula descends through the smooth Grassmann quotient. The definition's computation shows that replacing $(X,\eta )$ by $(XQ,\eta Q)$ changes $Y$ to $YQ$, leaving its range unchanged. Its identity differential from step 1.2 is therefore representative-independent.