I'm working through this script and I'm not sure if if there is a mistake at one point, or if I'm just thinking wrong.

To prove this, the group [itex]Sp(n+1) = \{A \in M(n+1, \mathbb H) | A^*A = I\}[/itex] is used. Its elements operate linearly and isometrically on [itex]\mathbb{S}^{4n+3}[/itex] and therefore induce isometries on [itex]\mathbb{HP}^n[/itex].

The proof starts by first defining two unit vectors [itex]v, w \in T_p \mathbb S^{4n+3}, p := (1, 0, ..., 0) \in \mathbb H^{n+1}.[/itex]. Now it says: "It suffices to find [itex]A \in Sp(n+1)[/itex] with [itex]A_*v = A_*w[/itex]."

Is this correct? Doesn't it have to say [itex]A_*v = w[/itex]? Wouldn't [itex]A_*v = A_*w[/itex] imply that [itex]v = w[/itex] since all matrices in the symplectic group are invertible?

[By the way, it goes on: "If we regard v, w as vectors in [itex]H^{n+1}[/itex] this problem is equivalent to: There is [itex]A \in Sp(n+1), Ap = p, Av = w[/itex]. Maybe this helps."]

I have a small follow up question. I hope it is ok that I post here again, as it is closely related to my first post.

Lateron, the curvature of [itex]\mathbb{CP}^n, \mathbb{HP}^n[/itex] is analyzed, namely:

Now it goes on:

And I don't see why such a matrix A necessarily exists. I mean, because of the statement in my first post, it is clear that there is a matrix A with [itex]A(p) = p, A_*(q) = A(q) = q[/itex]. And because it is an isometric diffeomorphism we still have [itex]A(q') \perp q \Rightarrow A(q') = (0, 0, s_3', s_4', ...)[/itex]. But I don't see how I can necessarily get [itex]A(q') = (0, 0, \lambda, 0, ...)[/itex]

Does it work to simply take A to be block diagonal of the form
[tex]
\left(
\begin{array}{cccc}
1 & & & \\
& 1 & & \\
& & \lambda/(q_3')^* & \\
& & & A'
\end{array}
\right)
[/tex]
for A' any Sp(n-3) matrix?

I don't think this matrix will necessarily be in Sp(n+1). Also, it is not guaranteed that [itex]q_3' \neq 0[/itex].

But I think I know how it works now. Your matrix gave me an idea:

Because [itex]Sp(n-1)[/itex] acts transitively on [itex]\mathbb S_{||q'||}^{4(n-1)-1}[/itex], there is a matrix [itex]A' \in Sp(n-1)[/itex] with [itex]A'(q_3', ..., q'_{n+1}) = (\lambda, 0, ..., 0), \lambda \in \mathbb R[/itex]. (Then [itex]|\lambda| = ||q'||[/itex].)

Then I can just take [itex]A(v_1, ..., v_{n+1}) := (v_1, v_2, A'(v_3, ..., v_{n+1}))[/itex]. This should be in [itex]Sp(n+1)[/itex] and have the desired properties :)