Classification of symmetric forms when every scalar is a square

A nondegenerate symmetric form over a field in which every element is a square is determined by its dimension and whether it is alternating. The alternating case uses symplectic bases; the other case uses orthonormal bases. In particular this applies over finite fields of characteristic two and separates the two kinds of symmetric pairing on elementary abelian two-groups.

References

• J. Milnor, D. Husemoller, Symmetric Bilinear Forms, Chapter I.

theorem LinearMap.BilinForm.IsSymm.equivalent_of_finrank_eq_of_isAlt_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {C : LinearMap.BilinForm K W} (hB : B.IsSymm) (hC : C.IsSymm) (hsq : ∀ (a : K), IsSquare a) (hndB : B.Nondegenerate) (hndC : C.Nondegenerate) (hdim : Module.finrank K V = Module.finrank K W) (halt : B.IsAlt ↔ C.IsAlt) : B.Equivalent C

Over a field in which every scalar is a square, nondegenerate symmetric forms of the same dimension and the same alternation type are equivalent.