The standard form of Proposition 30.6 (bilinear-form presentation).
The bilinear form on (F₂)^a × (F₂²)^b given by the orthogonal direct sum
of a copies of the rank-one form ⟨x, y⟩ ↦ ∑ xᵢ yᵢ (diagonal block) and
b copies of the hyperbolic plane ⟨x, y⟩ ↦ x₀y₁ + x₁y₀. Every
nondegenerate symmetric F₂-form is isometric to one of these
(see exists_isometry_standardF2Form).
Instances For
Case 1 of the inductive proof of Proposition 30.6. When the
nondegenerate symmetric F₂-form B admits a vector v with B v v ≠ 0
(necessarily B v v = 1), we split V = ⟨v⟩ ⊕ v^⊥, apply the inductive
hypothesis to v^⊥ (which is strictly smaller and inherits a nondegenerate
symmetric form), and reassemble the resulting isometry to gain an
additional diagonal ⟨1⟩ block.
The hyperbolic plane over F₂. The bilinear form on (F₂)² given
by ⟨x, y⟩ = x₀y₁ + x₁y₀; its Gram matrix is ⎡⎣0 1 / 1 0⎤⎦. This is
the basic building block, alongside ⟨1⟩, of the standard form in
Proposition 30.6, and it arises geometrically as the intersection form on
the middle cohomology of S² × S² with F₂ coefficients.
Instances For
Linear-equivalence rearrangement used in the inductive proof of
Proposition 30.6: identifies a hyperbolic-block factor (F₂²) with a new
first coordinate of (F₂²)^{b+1}, leaving the diagonal block unchanged.
This is the b-axis analogue of Fin.consLinearEquiv for the diagonal
block, used in case2_split to convert the inductive output into the
desired standard form.
Instances For
Case 2 of the inductive proof of Proposition 30.6. When the
nondegenerate symmetric F₂-form B is alternating (i.e. B v v = 0
for all v) on a nonzero space V, we pick any nonzero v and (using
nondegeneracy) a w with B v w = 1; the pair {v, w} then spans a
hyperbolic plane orthogonal complement. Splitting V = ⟨v, w⟩ ⊕ ⟨v, w⟩^⊥
and applying the inductive hypothesis to the orthogonal complement yields
an isometry with one additional hyperbolic block.
Inductive driver for Proposition 30.6 (auxiliary form by dimension).
Strong-induction statement on the dimension n of V: every nondegenerate
symmetric F₂-form on an n-dimensional F₂-vector space is isometric to
the standard block form standardF2Form a b. The base case n = 0 is the
unique zero form on the trivial space; the inductive step uses case1_split
when some v satisfies B v v ≠ 0 and case2_split when B is
alternating. This packages the induction so that the public version
exists_isometry_standardF2Form is a direct corollary.
Proposition 30.6 (Classification of nondegenerate symmetric bilinear
forms over F₂). Every nondegenerate symmetric bilinear form B on a
finite-dimensional F₂-vector space V is isometric to a standard
block-diagonal form standardF2Form a b: the orthogonal direct sum of a
copies of the rank-one form ⟨1⟩ and b copies of the hyperbolic plane.
The numbers a and b are determined (up to the standard mod-2 Witt
relation) by B; this is the mod-2 counterpart of Sylvester's law of
inertia and underlies the Wu-formula analysis of intersection forms of
closed 4-manifolds with F₂ coefficients.