Symplectic group as a regular level set
= Symplectic group as a regular level set
The map $F:M_{2n}(\mathbb R)\to\operatorname{Skew}_{2n}(\mathbb R)$ given by $F(A)=A^TJA$ has $Sp(2n,\mathbb R)=F^{-1}(J)$. At a symplectic $A$,
$$
DF_A(H)=H^TJA+A^TJH
$$
is surjective, so the <regular level set theorem> makes the symplectic group an embedded submanifold.