Diagonal quadratic forms

This file provides general infrastructure for diagonal quadratic forms expressed as weighted sums of squares.

Main results

• TauCeti.equivalent_weightedSumSquares_comp: reindexing the coefficients preserves equivalence.
• TauCeti.equivalent_weightedSumSquares_of_pair: a binary equivalence extends across fixed coordinates.
• QuadraticMap.associated_weightedSumSquares, QuadraticForm.toMatrix'_weightedSumSquares, and QuadraticForm.discr'_weightedSumSquares: over a ring in which two is invertible, the associated bilinear form of a diagonal form is the weighted dot product, its Gram matrix in the standard basis is the diagonal matrix of the weights, and its discriminant is their product.
• QuadraticMap.nondegenerate_weightedSumSquares: over a ring in which two is invertible, a diagonal form with regular weights is nondegenerate.
• QuadraticMap.weightedSumSquares_units: unit weights may be replaced by the scalars they name.
• QuadraticMap.not_anisotropic_weightedSumSquares_of_ternary_eq_zero: a ternary solution with a nonzero third coordinate gives a nonzero isotropic vector in a diagonal form.
• TauCeti.isSquare_prod_mul_prod_of_equivalent: isometric diagonal forms with unit weights have weight products differing by a square.

theorem TauCeti.equivalent_weightedSumSquares_of_pair {R : Type u} [CommSemiring R] {ι : Type v} [Fintype ι] {w w' : ι → R} {i j : ι} (hij : i ≠ j) (hpair : (QuadraticMap.weightedSumSquares R ![w i, w j]).Equivalent (QuadraticMap.weightedSumSquares R ![w' i, w' j])) (hrest : ∀ (k : ι), k ≠ i → k ≠ j → w k = w' k) : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R w')

Replacing two distinct coefficients by an equivalent binary form, while fixing all other coefficients, produces an equivalent diagonal form.

theorem TauCeti.equivalent_weightedSumSquares_comp {R : Type u} [CommSemiring R] {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] (w : ι → R) (σ : κ ≃ ι) : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R (w ∘ ⇑σ))

Reindexing the coefficients of a diagonal form does not change its equivalence class.

theorem QuadraticMap.weightedSumSquares_units {R : Type u} [CommSemiring R] {ι : Type v} [Fintype ι] (w : ι → Rˣ) : weightedSumSquares R w = weightedSumSquares R fun (i : ι) => ↑(w i)

A diagonal form with unit weights is the diagonal form with the underlying scalar weights.

@[simp]

theorem QuadraticMap.weightedSumSquares_apply_three_single {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (a : ι → R) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (x y z : R) : (weightedSumSquares R a) (Pi.single i x + Pi.single j y + Pi.single k z) = a i * x ^ 2 + a j * y ^ 2 + a k * z ^ 2

Evaluate a diagonal form on a linear combination of three distinct coordinate vectors.

theorem QuadraticMap.not_anisotropic_weightedSumSquares_of_ternary_eq_zero {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (a : ι → R) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) {x y z : R} (hz : z ≠ 0) (h : a i * x ^ 2 + a j * y ^ 2 + a k * z ^ 2 = 0) : ¬(weightedSumSquares R a).Anisotropic

A ternary solution with a nonzero third coordinate gives a nonzero isotropic vector in a diagonal quadratic form.

@[simp]

theorem QuadraticMap.associated_weightedSumSquares {R : Type u} [CommRing R] [Invertible 2] {ι : Type v} [Fintype ι] (w x y : ι → R) : ((associated (weightedSumSquares R w)) x) y = ∑ i : ι, w i * (x i * y i)

The bilinear form associated with a diagonal quadratic form pairs the coordinates diagonally: it is the weighted dot product.

@[simp]

theorem QuadraticForm.toMatrix'_weightedSumSquares {R : Type u} [CommRing R] [Invertible 2] {ι : Type v} [Fintype ι] [DecidableEq ι] (w : ι → R) : toMatrix' (QuadraticMap.weightedSumSquares R w) = Matrix.diagonal w

The matrix of a diagonal quadratic form in the standard basis is the diagonal matrix of its weights.

@[simp]

theorem QuadraticForm.discr'_weightedSumSquares {R : Type u} [CommRing R] [Invertible 2] {ι : Type v} [Fintype ι] [DecidableEq ι] (w : ι → R) : discr' (QuadraticMap.weightedSumSquares R w) = ∏ i : ι, w i

The discriminant of a diagonal quadratic form is the product of its weights.

theorem QuadraticMap.nondegenerate_weightedSumSquares {R : Type u} [CommRing R] [Invertible 2] {ι : Type v} [Fintype ι] {w : ι → R} (hw : ∀ (i : ι), IsRegular (w i)) : Nondegenerate

A diagonal form with regular weights is nondegenerate when two is invertible. Over a domain the hypothesis is that every weight is nonzero (isRegular_iff_ne_zero).

theorem TauCeti.isSquare_prod_mul_prod_of_equivalent {R : Type u} [CommRing R] [Invertible 2] {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] {w : ι → Rˣ} {v : κ → Rˣ} (h : (QuadraticMap.weightedSumSquares R w).Equivalent (QuadraticMap.weightedSumSquares R v)) : IsSquare ((∏ i : ι, w i) * ∏ i : κ, v i)

Isometric diagonal forms with unit weights have weight products differing by a square. An isometry of the coordinate spaces changes the Gram matrix of a diagonal form by a congruence, so it changes its determinant — the product of the weights — by the square of the determinant of that isometry.