Theorem. Witt extension and the regular-subspace interface [fcap-002A]

✍️sourceAGENTDRAFTED

Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) and \((V',Q')\) be isometric finite-dimensional nondegenerate quadratic spaces. If \(U\subseteq V\) is any subspace and \(f:U\to V'\) is an injective linear map satisfying \[Q'(f(u))=Q(u),\] then \(f\) extends to an isometry \(\widetilde f:(V,Q)\simeq (V',Q')\). For two subspaces of one quadratic space, the assumption that the ambient spaces are isometric is automatic.

[bourbaki2007algebra, Section 4, no. 3, Theorem 1, pp. 71--72] states the theorem with an arbitrary source subspace. In [serre1973course, Chapter IV, Section 1.5, Theorem 3, pp. 31--32], the proof explains why degeneracy of that subspace is harmless when the ambient form is nondegenerate: a radical vector can be paired with a new vector, enlarging the subspace toward a regular one. The regular case then splits orthogonally and closes by induction.

TauCeti proves a complementary form. For a finite-dimensional quadratic space over a field with \(2\) invertible, an isometry equivalence between subspaces \(W,W'\) extends when \(Q|_W\) is nondegenerate; the ambient form itself may be degenerate QuadraticMap.IsometryEquiv.exists_extension. It also chooses an extension and records its value on \(W\) QuadraticMap.IsometryEquiv.extension QuadraticMap.IsometryEquiv.extension_apply. These formal declarations do not prove the arbitrary-subspace statement above.

The distinction is visible inside \(Q_{1,3}\). The block \[A_0=\begin {pmatrix}5/4&3/4\\3/4&5/4\end {pmatrix}\] on the first positive and first negative coordinates, together with the identity on the other two coordinates, defines an ambient isometry \(A\). It satisfies \(A(e_0+e_1)=2(e_0+e_1)\), so its restriction to the null line is an isometry of a degenerate subspace. The classical theorem covers such a line; the regular-subspace formal declaration does not apply because the source restriction is degenerate.