Negative semidefiniteness from a positive null vector

Let A be a symmetric matrix over a linear ordered field whose off-diagonal entries are nonnegative, and suppose that A kills a vector m with strictly positive entries. Then the quadratic form of A is negative semidefinite, and when the positive-entry graph of A is connected it vanishes exactly on the multiples of m (Stacks, Tag 0C5X).

The intersection matrix of the special fibre of a regular model of a curve over a discrete valuation ring has this shape, with m the vector of multiplicities of the components. The statement is the source of the negative definiteness of the intersection form on vectors supported on a proper subset of the components, which drives the classification of configurations of components.

The proof is the first proof of the Stacks Project: writing x = (yᵢ mᵢ)ᵢ, the relation A m = 0 turns the quadratic form into 2 xᵀ A x = -∑ᵢⱼ aᵢⱼ mᵢ mⱼ (yᵢ - yⱼ)², in which every term with i ≠ j is nonnegative and every term with i = j vanishes.

Main results

• Matrix.two_mul_dotProduct_mulVec_eq_neg_sum: the identity above, stated without dividing the entries of x.
• Matrix.dotProduct_mulVec_nonpos_of_mulVec_eq_zero: the quadratic form is negative semidefinite.
• Matrix.dotProduct_mulVec_eq_zero_iff_of_mulVec_eq_zero: under connectedness, its isotropic vectors are exactly the multiples of m.

theorem Matrix.two_mul_dotProduct_mulVec_eq_neg_sum {C : Type u_1} {K : Type u_2} [Fintype C] [Field K] {A : Matrix C C K} (hA : A.IsSymm) {m : C → K} (hm : ∀ (i : C), m i ≠ 0) (hAm : A.mulVec m = 0) (x : C → K) : 2 * x ⬝ᵥ A.mulVec x = -∑ i : C, ∑ j : C, A i j * (m j * x i - m i * x j) ^ 2 / (m i * m j)

If a symmetric matrix A over a field kills a vector m with nonzero entries, then its quadratic form is 2 xᵀ A x = -∑ᵢⱼ aᵢⱼ (mⱼxᵢ - mᵢxⱼ)² / (mᵢmⱼ).

theorem Matrix.dotProduct_mulVec_nonpos_of_mulVec_eq_zero {C : Type u_1} {K : Type u_2} [Fintype C] [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix C C K} (hA : A.IsSymm) (hnonneg : ∀ (i j : C), i ≠ j → 0 ≤ A i j) {m : C → K} (hm : ∀ (i : C), 0 < m i) (hAm : A.mulVec m = 0) (x : C → K) : x ⬝ᵥ A.mulVec x ≤ 0

The quadratic form of a symmetric matrix over a linear ordered field with nonnegative off-diagonal entries is negative semidefinite as soon as the matrix kills a vector with positive entries (Stacks, Tag 0C5X).

theorem Matrix.dotProduct_mulVec_eq_zero_iff_of_mulVec_eq_zero {C : Type u_1} {K : Type u_2} [Fintype C] [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix C C K} (hA : A.IsSymm) (hnonneg : ∀ (i j : C), i ≠ j → 0 ≤ A i j) (hconnected : ∀ (i j : C), Relation.ReflTransGen (fun (i j : C) => i ≠ j ∧ 0 < A i j) i j) {m : C → K} (hm : ∀ (i : C), 0 < m i) (hAm : A.mulVec m = 0) (x : C → K) : x ⬝ᵥ A.mulVec x = 0 ↔ ∃ (c : K), x = c • m

Let A be a symmetric matrix over a linear ordered field with nonnegative off-diagonal entries and connected positive-entry graph, killing a vector m with positive entries. Then its quadratic form vanishes exactly on the multiples of m (Stacks, Tag 0C5X).