I am trying to use the implicit function theorem to prove that $Sp(4,\mathbb{R})$ is a Lie group. I have defined the map $f:M_{4\times 4}(\mathbb{R}) \to \mathit{Skew}_{\mkern 1.5mu 4\times4}$ by $f(X) = XJX^T$, where
$$J = \begin{bmatrix} 0_{2\times2} & I_{2\times 2} \\ -I_{2\times 2} & 0_{2\times 2} \end{bmatrix} $$
Then, I get that $Sp(4,\mathbb{R}) = f^{-1}(J)$. Now, I need to show that
$$\left. f_*\right|_X :T_X M_{4\times 4} \to T_{f(X)} \mathit{Skew}_{\mkern1.5mu 4\times4}$$
is surjective. Does anyone have any advice on how I might be able to do this? Thanks.
There is a canonical isomorphism $T_X\mathcal{M}_{4\times 4}(\mathbb{R}) \cong \mathcal{M}_{4\times 4}(\mathbb{R})$, $T_{f(X)}Skew_{4 \times 4} \cong Skew_{4 \times 4}$ such that
$(d_Xf)(Y)=XJY^t-YJX^t=-2\pi(YJX^t)$ where $\pi$ is the natural projection on $Skew_{4 \times 4}$.
Now, what can you say about $Y \longmapsto YJX^t$ if $X$ is symplectic?