Quadratic forms over a separably closed field

This file proves that a finite-dimensional nondegenerate quadratic form over a separably closed field of characteristic different from two is equivalent to a sum of squares, so that such forms are classified up to equivalence by their dimension.

Main results

• QuadraticForm.equivalent_weightedSumSquares_of_isSepClosed: a nondegenerate quadratic form is equivalent to the standard sum of squares.
• QuadraticForm.equivalent_of_finrank_eq_of_isSepClosed: nondegenerate quadratic forms on spaces of the same dimension are equivalent.

References

• Mathlib's QuadraticForm.isometryEquivSumSquaresUnits and QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed supply the normalization argument adapted here from algebraically closed to separably closed fields.

theorem QuadraticForm.equivalent_weightedSumSquares_of_isSepClosed {K : Type u_2} [Field K] [IsSepClosed K] [Invertible 2] {M : Type u_3} [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K 1)

A finite-dimensional nondegenerate quadratic form over a separably closed field of characteristic different from two is equivalent to the standard sum of squares.

theorem QuadraticForm.equivalent_of_finrank_eq_of_isSepClosed {K : Type u_2} [Field K] [IsSepClosed K] [Invertible 2] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module K M] [FiniteDimensional K M] [AddCommGroup N] [Module K N] [FiniteDimensional K N] (Q : QuadraticForm K M) (R : QuadraticForm K N) (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (h : Module.finrank K M = Module.finrank K N) : QuadraticMap.Equivalent Q R

Nondegenerate quadratic forms over a separably closed field of characteristic different from two, on possibly different finite-dimensional spaces, are equivalent when their dimensions agree.