Quadratic forms over an algebraically closed field

equivalent_sum_squares: A nondegenerate quadratic form over an algebraically closed field of characteristic not equal to 2 is equivalent to a sum of squares.

TODO: generalize QuadraticForm.isometryEquivSumSquares to quadratically closed field.

noncomputable def QuadraticForm.isometryEquivSumSquares {ι : Type u_1} [Fintype ι] {K : Type u_2} [Field K] [IsAlgClosed K] [DecidableEq K] (w : ι → K) : (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K fun (i : ι) => if w i = 0 then 0 else 1)

The isometry between a weighted sum of squares on an algebraically closed field and the sum of squares, i.e. weightedSumSquares with weights 1 or 0.

Equations

• QuadraticForm.isometryEquivSumSquares w = QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares (fun (i : ι) => if h : w i = 0 then 1 else Units.mk0 ⋯.choose ⋯) ⋯

noncomputable def QuadraticForm.isometryEquivSumSquaresUnits {ι : Type u_1} [Fintype ι] {K : Type u_2} [Field K] [IsAlgClosed K] [DecidableEq K] (w : ι → Kˣ) : (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K 1)

The isometry between a weighted sum of squares on an algebraically closed field and the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

Equations

• QuadraticForm.isometryEquivSumSquaresUnits w = (QuadraticForm.isometryEquivSumSquares fun (i : ι) => ↑(w i)).trans (QuadraticForm.weightedSumSquaresCongr ⋯)

theorem QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed {K : Type u_2} [Field K] [IsAlgClosed 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 nondegenerate quadratic form on an algebraically closed field of characteristic not equal to 2 is equivalent to the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

theorem QuadraticForm.equivalent_of_isAlgClosed {K : Type u_2} [Field K] [IsAlgClosed K] [Invertible 2] {M : Type u_3} [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q₁ Q₂ : QuadraticForm K M) (hQ₁ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₁)) (hQ₂ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₂)) : QuadraticMap.Equivalent Q₁ Q₂

All nondegenerate quadratic forms on an algebraically closed field of characteristic not equal to 2 are equivalent.