QuadraticForm.equivalent_sum_squares
theorem QuadraticForm.equivalent_sum_squares :
∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℂ M] [inst_2 : FiniteDimensional ℂ M]
(Q : QuadraticForm ℂ M),
LinearMap.SeparatingLeft (QuadraticForm.associated Q) → Q.Equivalent (QuadraticForm.weightedSumSquares ℂ 1)
The theorem `QuadraticForm.equivalent_sum_squares` states that for a nondegenerate quadratic form over the complex numbers (ℂ) on a given module (which is a finite-dimensional vector space over ℂ), the quadratic form is equivalent to a weighted sum of squares with unit weights. This equivalence is established under the condition that the associated bilinear form of the quadratic form is separating on the left. In other words, every nondegenerate quadratic form can be expressed as a sum of squares in the complex number domain when the associated bilinear form is a separating form.
More concisely: A nondegenerate quadratic form over the complex numbers is equivalent to a weighted sum of squares with unit weights through its separating bilinear form.
|
QuadraticForm.complex_equivalent
theorem QuadraticForm.complex_equivalent :
∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℂ M] [inst_2 : FiniteDimensional ℂ M]
(Q₁ Q₂ : QuadraticForm ℂ M),
LinearMap.SeparatingLeft (QuadraticForm.associated Q₁) →
LinearMap.SeparatingLeft (QuadraticForm.associated Q₂) → Q₁.Equivalent Q₂
The theorem `QuadraticForm.complex_equivalent` states that for any two nondegenerate quadratic forms, `Q₁` and `Q₂`, on a finite-dimensional vector space `M` over the complex numbers, if the symmetric bilinear forms associated with `Q₁` and `Q₂` (obtained through the linear map `QuadraticForm.associated`) are separating (that is, nondegenerate), then `Q₁` and `Q₂` are equivalent. This is to say that all nondegenerate quadratic forms on vector spaces over the complex numbers are equivalent if their associated symmetric bilinear forms are nondegenerate.
More concisely: If two nondegenerate complex quadratic forms have separating (nondegenerate) associated symmetric bilinear forms, then they are equivalent.
|