Question
Write $(2n\times 2n)$-matrices in block form
$A=\begin{bmatrix}a&b\\c&d\end{bmatrix} \in Mat_{\mathbb{R}}(2n)$
where each of $a,b,c,d$ is an $n\times n$ block. Define
$J=\begin{bmatrix}0&1\\-1&0\end{bmatrix}$
where 1 is a shorthand for an $n\times n$ identity matrix. Let
$Sp(2n)= \{ A\in Mat_\mathbb{R}(2n)| AJA^T=J \}$,
so that $Sp(2n)=F^{-1}J$, where $F: Mat_{\mathbb{R}}(2n)\rightarrow Skew_{\mathbb{R}}(2n)$ is the map $F(A)=AJA^T$. Here, the codomain is the set of real $n\times n$ matrices satisfying $C=-C^T$.
(I have already shown that the differential $D_AF: Mat_{\mathbb{R}}(2n)\rightarrow Skew_{\mathbb{R}}(2n)$ is $AJH^T+HJA^T$)
Show that for $A\in F^{-1}(J)$, the differential is surjective, and conclude that $F^{-}(J)$ is a submanifold. What is its dimension?
Note I can’t seem to show the differential is surjective. I know once that is settled, the case of sub-manifold will be easy to handle. I think the dimension is easy to
By your calculation of the differential $$ D_A F: Mat_{\mathbb R}(2n)\to Skew_{\mathbb R}(2n);\ H\mapsto AJH^T + HJA^T, $$ we would like to show that for $A\in F^{-1}J=Sp(2n)$ and $C\in Skew_{\mathbb R}(2n)$ with $C=-C^T$, there exists an $H$ such $D_A F(H)=C$.
Note that $A\in F^{-1}J$ is invertible, since $$ AJA^T=J\ \Longrightarrow\ A(JA^TJ^{-1})=I\ \Longrightarrow\ A^{-1}\text{ exists}. $$ Then $JA^T=A^{-1}J$.
The key is that both $D_AF(H)$ and $C$ are skew-symmetric. Indeed, $$(HJA^T)^T=AJ^TH^T=-AJH^T.$$ We can let $$ HJA^T=\frac{1}{2}C, $$ then $AJH^T=-(HJA^T)^T=-\frac{1}{2}C^T=\frac{1}{2}C.$ So the equation is solved.
Therefore we have a solution to $D_AF(H)=C$ as $$ H=\frac{1}{2}C(JA^T)^{-1}=\frac{1}{2}C(A^{-1}J)^{-1}=\frac{1}{2}CJ^{-1}A = -\frac{1}{2}CJA, $$ since $J^{-1}=-J$.
This solution can be directly checked, using $AJA^T=J$.