Let us consider the quaternionic non-commutative field $\mathbf{H} = \mathbf{R}^4$ and its projective space $\mathbf{P}_1(\mathbf{H})$ of dimension 1, which is, by definition, the set of lines in $\mathbf{H}$ passing through the origin endowed with the unique structure of differential manifold for which the canonical left-action of the linear group $\mathbf{GL}(1; \mathbf{H})$ (where $\mathbf{H}^d$ is considered as a left-module over $\mathbf{H}$ for every $d \in \mathbf{N}$) on $\mathbf{H}$ (the canonical action is, of course, $(s, L) \mapsto s(L)$) is of class $\mathscr{C}^\infty.$
I want to understand the proof of the diffeomorphism between $\mathbf{P}_1(\mathbf{H})$ with $\mathbf{S}_4$ (the unit sphere in $\mathbf{R}^5$).
I sketch the proof now. Consider a point $(x, y) \in \mathbf{S}_7 \subset \mathbf{R}^8 = \mathbf{R}^4 \times \mathbf{R}^4.$ Write $x = x_0 + ix_1 + jx_2 + kx_3$ and similarly for $y;$ define $$f(x, y) = (2x \bar{y}, \|x\|^2 - \|y\|^2) = z = (z_0, z_1, z_2, z_3, z_4) \in \mathbf{H} \times \mathbf{R} = \mathbf{R}^5.$$ Since $\|(x, y)\| = 1,$ it turns out $z_4 = 2\|x\|^2 - 1$ and for such $z_4 \in (-1, 1)$ given, the point $2x \bar{y}$ can be any in the sphere of radius $\|2x \bar{y}\|^2 = 4 \|x\|^2 \|y\|^2 = (z_4+1)(1-z_4)=1-z_4^2,$ hence $f(x, y) = z \in \mathbf{S}_4$ and $f:\mathbf{S}_7 \to \mathbf{S}_4$ is a surjective $\mathscr{C}^\infty$-function.
I already know that there exists a canonical submersion $\mathbf{S}_7 \xrightarrow{\pi} \mathbf{P}_1(\mathbf{H})$ such that two points in $(x, y)$ and $(x', y')$ in $\mathbf{S}_7$ are identified if there exists a quaternion $q$ such that $(x, y) = (x'q, y'q) = (x', y') q$ (where we are identifying some vector with matrices in the go, all using canonical bases). Now, observe that $f(x, y) = f(x', y')$ signifies $z = z'$ which is the same as the two relations $$x\bar{y} = x' \bar{y}' \quad \text{ and } \quad 2\|x\|^2-1=2\|x'\|^2-1$$ and these imply that $\|x\| = \|x'\|$ so that $x' = x q$ for some quaternion $q$ of norm $1$ and then $x\bar{y} = x' \bar{y}' = x q \bar{y}'$ implying $\bar{y} = q\bar{y}'$ or $y' = y \bar{q}^{-1} = y q.$ That is to say, $f$ can be factorised: $$f:\mathbf{S}_7 \xrightarrow{\pi} \mathbf{P}_1(\mathbf{H}) \xrightarrow{g} \mathbf{S}_4,$$ where $g$ is a bijection, with no differentiability properties a priori.
Since $f$ is of class $\mathscr{C}^\infty$ as well as $\pi$ and since $\pi$ is a submersion, we know that $g$ is of class $\mathscr{C}^\infty.$ Hence, if we show $f$ is a submersion, then $g$ would have to be a submersion. If we had this ($g$ being a bijective submersion), it would turn out that $g$ is the desired diffeomorphism!
Here is the crux I cannot solve myself. How to show $f$ is a submersion $\mathbf{S}_7 \to \mathbf{S}_4$?
Any help appreciated.
Here is the answer I came up with.
I want to show $f$ is a submersion. Observe that $t \mapsto t^2$ is a diffeomorphism of $\mathbf{R}^*_+$ onto itself and that the function $\tilde f,$ which is just $f$ extendend to $\mathbf{R}^8-\{0\}$, satisfies $f(tx, ty) = t^2 f(x, y)$ and this says that $\tilde f$ factorises as $\mathbf{R}^8 \setminus -\{0\} \to \mathbf{R}_+^* \times \mathbf{S}_8 \to \mathbf{R}^*_+ \times \mathbf{S}_4 \to \mathbf{R}^5,$ the arrow in the middle being of the form $\varphi \times f,$ where $u \times v$ denotes the function $(s,t) \mapsto (u(s), v(t)).$ Hence, if $\tilde f$ had rank 5 everywhere, since the diffeomorphism $t \mapsto t^2$ has rank 1 everywhere, it would turns out that $f$ has rank 4. But showing $\tilde f$ has rank 5 is relatively easy.
1) Consider the functions $(x,y) \mapsto (px, qy)$ for fixed quaternions $p$ and $q,$ these functions are diffeomorphism of $\mathbf{S}_7$ onto itself and it transforms $x\bar y$ into $px \bar y \bar q$ and we can are reduced to show $\tilde f$ has rank 5 at the points of the form $(x, y)$ in $\mathbf{R}^8$ where $x$ and $y$ represent scalars (equivalently, $(x, y) = (x_0, 0,0,0, y_0,0,0,0).$
2) With these reductions, $f'(x, y)$ (with $x$ and $y$ as before) is easily calculable and its rank is readily seen to be 5.