Documentation

Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

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.

source
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      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.

      source
      📐 coverage
      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.