Quadratic forms over the complex numbers #
equivalent_sum_squares: A nondegenerate quadratic form over the complex numbers is equivalent to
a sum of squares.
noncomputable def
QuadraticForm.isometryEquivSumSquares
{ι : Type u_1}
[Fintype ι]
(w' : ι → ℂ)
:
(QuadraticMap.weightedSumSquares ℂ w').IsometryEquiv
(QuadraticMap.weightedSumSquares ℂ fun (i : ι) => if w' i = 0 then 0 else 1)
The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. weightedSumSquares with weights 1 or 0.
Equations
- QuadraticForm.isometryEquivSumSquares w' = ⋯.mpr ((QuadraticMap.weightedSumSquares ℂ w').isometryEquivBasisRepr ((Pi.basisFun ℂ ι).unitsSMul fun (i : ι) => ⋯.unit))
Instances For
noncomputable def
QuadraticForm.isometryEquivSumSquaresUnits
{ι : Type u_1}
[Fintype ι]
(w : ι → ℂˣ)
:
(QuadraticMap.weightedSumSquares ℂ w).IsometryEquiv (QuadraticMap.weightedSumSquares ℂ 1)
The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.
Equations
- QuadraticForm.isometryEquivSumSquaresUnits w = ⋯.mp (QuadraticForm.isometryEquivSumSquares (Units.val ∘ w))
Instances For
theorem
QuadraticForm.equivalent_sum_squares
{M : Type u_2}
[AddCommGroup M]
[Module ℂ M]
[FiniteDimensional ℂ M]
(Q : QuadraticForm ℂ M)
(hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q))
:
A nondegenerate quadratic form on the complex numbers is equivalent to
the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.
theorem
QuadraticForm.complex_equivalent
{M : Type u_2}
[AddCommGroup M]
[Module ℂ M]
[FiniteDimensional ℂ M]
(Q₁ Q₂ : QuadraticForm ℂ M)
(hQ₁ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₁))
(hQ₂ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₂))
:
QuadraticMap.Equivalent Q₁ Q₂
All nondegenerate quadratic forms on the complex numbers are equivalent.