Symplectic transvections generate the binary symplectic group

For $s\in \{0,1,2,3\}$, the standard coordinate vectors form a basis of ${\mathbb{F}}_2^s$ by coordinate expansion and coordinatewise independence, so $\dim {\mathbb{F}}_2^s=s$. Let $d\in \{2,3\}$ and let $U$ be a proper subspace of ${\mathbb{F}}_2^d$. Since $U$ is finite, choose a linearly independent subset $B\subseteq U$ maximal under inclusion; maximality makes it span $U$, since any vector outside its span could be adjoined while preserving independence. If $r=\mathrm{\mid }B\mathrm{\mid }$, its $2^r$ binary coefficient lists give distinct vectors by independence and exhaust $U$ by spanning, so $\mathrm{\mid }U\mathrm{\mid }=2^r$. But $\mathrm{\mid }{\mathbb{F}}_2^d\mathrm{\mid }=2^d$ and $U$ is proper, hence $r<d$. Enumerate $B=(q_1,\dots ,q_r)$ and define $A_B:{\mathbb{F}}_2^d\to {\mathbb{F}}_2^r$ by $A_B(\alpha )=(\alpha \cdot q_1,\dots ,\alpha \cdot q_r)$. Each coordinate dot product is linear in $\alpha$, so $A_B$ is linear [F4]. Its domain and codomain have dimensions $d$ and $r$ by the coordinate-basis calculation. Its image is a finite subspace; a maximal independent subset spans it as above, and its $2^{\mathrm{rank}{A}_B}$ distinct binary combinations lie among the $2^r$ vectors of ${\mathbb{F}}_2^r$, so its rank is at most $r$. Thus rank-nullity [F2] gives $\dim \ker A_B=d-\mathrm{rank}{A}_B\ge d-r>0$. For nonzero $\alpha \in \ker A_B$, every basis vector $q_i$ satisfies $\alpha \cdot q_i=0$, so linearity and spanning give $\alpha \cdot u=0$ for every $u\in U$. The functional $u\mapsto \alpha \cdot u$ is nonzero because its value on a coordinate vector with nonzero corresponding coordinate of $\alpha$ is $1$.

Alternation and bilinearity imply $0=\omega (u+w,u+w)=\omega (u,w)+\omega (w,u)$ for all $u,w$; since subtraction equals addition in ${\mathbb{F}}_2$, $\omega$ is symmetric. For $v=0$, ${\tau }_v$ is the identity. For any $v$, alternation gives $\omega (v,v)=0$, so applying ${\tau }_v$ twice adds $\omega (w,v)v$ twice and returns $w$. For $u,w\in V$, bilinearity gives $\omega ({\tau }_{v}u,{\tau }_{v}w)=\omega (u,w)+\omega (w,v)\omega (u,v)+\omega (u,v)\omega (v,w)\mathrm{.}$ Symmetry from the first sentence makes the last two terms the same product, which sums to zero in ${\mathbb{F}}_2$; therefore ${\tau }_v$ preserves $\omega$.

At $n=0$, $\dim V=0$ implies $V=\{0\}$ by [F3]. Its identity is the only symplectic map and is the empty composition of transvections.

These maps act transitively on nonzero vectors. If $a=b$, no map is needed. If $\omega (a,b)=1$, then $v=a+b$ satisfies $\omega (a,v)=1$, hence ${\tau }_v(a)=b$. If $a\mathrm{\ne }b$ and $\omega (a,b)=0$, then $a,b$ are independent over ${\mathbb{F}}_2$. Their pairing functionals are independent: a relation $r\omega (a,\cdot )+s\omega (b,\cdot )=0$ gives $\omega (ra+sb,w)=0$ for every $w$, so nondegeneracy gives $ra+sb=0$, and independence gives $r=s=0$. The map $L(w)=(\omega (a,w),\omega (b,w))$ is linear by bilinearity. If its image were proper, step 1.1 would give a nonzero $\alpha \in {\mathbb{F}}_2^2$ with $\alpha \cdot L(w)=0$ for every $w$. This would make a nontrivial linear combination of the pairing functionals zero, a contradiction. Thus $L$ is onto; choose $c$ with both pairings $1$. By symmetry from step 1.2, $\omega (c,b)=1$, so ${\tau }_{a+c}(a)=c$ and ${\tau }_{c+b}(c)=b$.

Fix $e,f$ with $\omega (e,f)=1$. If $y$ and $f$ both pair to $1$ with $e$, then transvections fixing $e$ send $y$ to $f$ as follows. If $y=f$, use the identity. If $\omega (y,f)=1$, the center $y+f$ lies in $e^{\perp }$ and ${\tau }_{y+f}(y)=f$. If $y\mathrm{\ne }f$ and $\omega (y,f)=0$, the vectors $e,y,f$ are independent: pairing a relation $re+sy+tf=0$ with $e$ gives $s=t$ by symmetry from step 1.2; if $s=t=1$, then $y+f=re$, which would give either $y=f$ or $\omega (y,f)=\omega (f+re,f)=r=1$, both impossible. Their pairing functionals are independent because a relation among them is the pairing with the corresponding linear combination of $e,y,f$, which nondegeneracy forces to be zero. The map $L(w)=(\omega (e,w),\omega (y,w),\omega (f,w))$ is linear by bilinearity. If its image were proper, step 1.1 would give a nonzero $\alpha \in {\mathbb{F}}_2^3$ annihilating every value of $L$, contradicting independence of the three pairing functionals. Hence $L$ is onto; choose $c$ with all three values $1$. The centers $y+c$ and $c+f$ lie in $e^{\perp }$, and ${\tau }_{c+f}{\tau }_{y+c}(y)=f$; both transvections fix $e$.

Assume $n\ge 1$ and the result for dimension $2(n-1)$. For the application $V=V_n$, the nondegenerate alternating form hypotheses hold by [F1]; the following argument is for any such $V$. Since $\dim V=2n>0$, choose $e\mathrm{\ne }0$; nondegeneracy gives $f$ with $\omega (e,f)=1$. Let $T_0$ be symplectic. By step 2.1, choose a finite product $A$ of transvections with $A(T_{0}e)=e$, and set $T_1=A{T}_0$. The vector $y=T_{1}f$ satisfies $\omega (e,y)=1$, so step 3.1 gives a finite product $B$ of transvections fixing $e$ and sending $y$ to $f$. Thus $G=B{T}_1$ is symplectic and fixes both $e$ and $f$. Let $W=\{w:\omega (w,e)=\omega (w,f)=0\}$. Bilinearity makes $W$ a subspace and $\mathrm{\Phi }:V\to {\mathbb{F}}_2^2$, $\mathrm{\Phi }(u)=(\omega (u,f),\omega (u,e))$, linear by [F4]; it is onto because $\mathrm{\Phi }(e)=(1,0)$ and $\mathrm{\Phi }(f)=(0,1)$, and its kernel is $W$. Step 1.1 gives $\dim {\mathbb{F}}_2^2=2$, so rank-nullity [F2] yields $\dim W=\dim V-2=2(n-1)$. For any $u$, bilinearity and $\omega (e,f)=1$ show that $w=u+\omega (u,f)e+\omega (u,e)f$ lies in $W$, so every $u$ is a sum of an element of $E=\{re+sf:r,s\in {\mathbb{F}}_2\}$ and an element of $W$; the intersection is zero since pairing $re+sf\in W$ with $f$ and $e$ gives $r=s=0$. Thus $V=E\oplus W$. The restriction of $\omega$ to $W$ is nondegenerate: a vector in its radical is orthogonal to $W,e,f$, hence to all of $V$, and is zero. Since $G$ and $G^{-1}$ fix $e,f$ and preserve $\omega$, both map $W$ to itself, so $G{\mathrm{\mid }}_W$ is an invertible symplectic map. By the induction hypothesis, $G{\mathrm{\mid }}_W$ is a finite product of transvections centered in $W$. Those same transvections fix $e,f$ in $V$ and agree with $G$ on $W$, so their product is $G$ on $V=E\oplus W$. Since each transvection is its own inverse by step 1.2, $T_0=A^{-1}{B}^{-1}G$ is a finite product of transvections. All choices are finite-stage existential choices; the proof uses no choice principle.