The real symplectic matrix group

Let ${\mathrm{Skew}}_{2n}(\mathbb{R})$ be the vector space of skew-symmetric matrices and define $F:{\mathrm{GL}}_{2n}(\mathbb{R})\to {\mathrm{Skew}}_{2n}(\mathbb{R})$ by $F(A)=A^{T}JA$; the codomain is correct because $J^T=-J$. Then $d{F}_A(X)=X^{T}JA+A^{T}JX$. At a point of $F^{-1}(J)$ write $X=AZ$; then the differential is $Z^{T}J+JZ$. Every skew-symmetric $S$ occurs by taking $Z=\frac{1}{2}{J}^{-1}S$. Hence the differential is surjective onto its stated codomain along the level, and [F3] makes it embedded.

The equations $(AB{)}^{T}J(AB)=J$ and $(A^{-1}{)}^{T}J{A}^{-1}=J$ show that the level is a subgroup, so [F1] makes it a Lie group. At $I$, the tangent kernel from step 1.1 is exactly $X^{T}J+JX=0$.

If $X$ and $Y$ satisfy that equation, direct expansion gives $(XY-YX{)}^{T}J+J(XY-YX)=0$, so the tangent space is closed under the commutator bracket.

For $n=0$ the group is trivial. Singular tangent matrices are allowed, while group matrices are invertible because the defining equation gives an explicit inverse. No interval, endpoint, metric choice, or biconditional occurs. ${\mathrm{A}\mathrm{C}}_{\omega }$ is propagated only through [F1].