The intersection form of a numerical type

The intersection matrix A = (aᵢⱼ) of a numerical type is symmetric, has nonnegative off-diagonal entries and a connected graph, and kills the positive multiplicity vector m. Its quadratic form x ↦ xᵀ A x is therefore negative semidefinite, and it vanishes exactly on the rational multiples of m (Stacks, Tag 0C5X). Since m has no zero entry, the form is negative definite on the vectors that vanish at some component, that is, on the vectors supported on a proper subset of the components. In particular every proper principal submatrix of A is negative definite. Written out, this gives aᵢⱼ² < aᵢᵢ aⱼⱼ for two distinct components i and j of a numerical type with more than two components, a negative determinant for the 3 × 3 submatrix on three distinct components of a numerical type with more than three components, and a positive determinant for the 4 × 4 submatrix on four distinct components of a numerical type with more than four components. On five components the determinant is not the convenient form: what the classification uses there is the value of the form itself at an explicit vector.

These are the inputs of the classification of configurations of (-2)-indices in Stacks, Section 0C7L, which in turn bounds the multiplicities of a minimal numerical type.

Main results

• TauCeti.NumericalType.dotProduct_intersection_mulVec_nonpos: xᵀ A x ≤ 0.
• TauCeti.NumericalType.dotProduct_intersection_mulVec_eq_zero_iff: xᵀ A x = 0 exactly when the cross-products mⱼ xᵢ = mᵢ xⱼ agree, i.e. when x is proportional to m.
• TauCeti.NumericalType.dotProduct_intersection_mulVec_neg: xᵀ A x < 0 for a nonzero x vanishing at some component.
• TauCeti.NumericalType.dotProduct_intersection_mulVec_of_support_subset: xᵀ A x is the sum over the principal submatrix carrying the support of x.
• TauCeti.NumericalType.sum_sum_intersection_mul_neg: the same sum is negative for a nonzero vector on a proper finite set of components.
• TauCeti.NumericalType.not_forall_fintype_sum_intersection_mul_nonneg_of_pos: a nonnegative, nonzero vector on a proper finite family of distinct components has a row with negative intersection sum.
• TauCeti.NumericalType.not_forall_sum_intersection_mul_nonneg_of_pos: the specialization to a family indexed by an initial segment of the natural numbers.
• TauCeti.NumericalType.intersection_sq_lt_intersection_mul_intersection: aᵢⱼ² < aᵢᵢ aⱼⱼ for distinct components when there are more than two components.
• TauCeti.NumericalType.intersection_det_triple_neg: the determinant of the principal 3 × 3 submatrix on three distinct components is negative when there are more than three components.
• TauCeti.NumericalType.intersection_det_four_pos: the determinant of the principal 4 × 4 submatrix on four distinct components is positive when there are more than four components.
• TauCeti.NumericalType.intersection_five_neg: the intersection form at a vector supported on five distinct components, written out, is negative when there are more than five components.
• TauCeti.NumericalType.intersection_six_neg: the analogous formula for six components.

The intersection matrix over ℚ

Semidefiniteness

theorem TauCeti.NumericalType.dotProduct_intersection_mulVec_nonpos (T : NumericalType) (x : T.Component → ℤ) : x ⬝ᵥ T.intersection.mulVec x ≤ 0

The intersection form of a numerical type is negative semidefinite (Stacks, Tag 0C5X).

theorem TauCeti.NumericalType.dotProduct_intersection_mulVec_eq_zero_iff (T : NumericalType) (x : T.Component → ℤ) : x ⬝ᵥ T.intersection.mulVec x = 0 ↔ ∀ (i j : T.Component), ↑↑(T.multiplicity j) * x i = ↑↑(T.multiplicity i) * x j

The intersection form of a numerical type vanishes at an integral vector exactly when the vector is proportional to the multiplicity vector, that is, when its cross-products with the multiplicity vector agree (Stacks, Tag 0C5X).

theorem TauCeti.NumericalType.dotProduct_intersection_mulVec_neg (T : NumericalType) {x : T.Component → ℤ} (hx : x ≠ 0) {i : T.Component} (hi : x i = 0) : x ⬝ᵥ T.intersection.mulVec x < 0

The intersection form of a numerical type is negative definite on the vectors vanishing at some component, that is, on the vectors supported on a proper subset of the components.

theorem TauCeti.NumericalType.dotProduct_intersection_mulVec_of_support_subset (T : NumericalType) {s : Finset T.Component} {x : T.Component → ℤ} (hx : ∀ i ∉ s, x i = 0) : x ⬝ᵥ T.intersection.mulVec x = ∑ i ∈ s, ∑ j ∈ s, T.intersection i j * x i * x j

The intersection form evaluated at a vector supported on a finite set of components is the corresponding sum over the principal submatrix on that set.

theorem TauCeti.NumericalType.sum_sum_intersection_mul_neg (T : NumericalType) {s : Finset T.Component} (hs : s ≠ Finset.univ) {y : T.Component → ℤ} (hy : ∃ i ∈ s, y i ≠ 0) : ∑ i ∈ s, ∑ j ∈ s, T.intersection i j * y i * y j < 0

The intersection form of a numerical type is negative definite on the vectors supported on a proper subset of the components: if s is a finite set of components which is not all of them and y does not vanish identically on s, then ∑_{i, j ∈ s} aᵢⱼ yᵢ yⱼ < 0.

theorem TauCeti.NumericalType.not_forall_fintype_sum_intersection_mul_nonneg_of_pos (T : NumericalType) {I : Type u_1} [Fintype I] {e : I → T.Component} (he : Function.Injective e) (hcard : Fintype.card I < Fintype.card T.Component) {y : I → ℤ} (hy : ∀ (i : I), 0 ≤ y i) (hypos : ∃ (i : I), 0 < y i) : ¬∀ (i : I), 0 ≤ ∑ j : I, T.intersection (e i) (e j) * y j

A nonnegative, nonzero integral vector on a proper finite family of distinct components cannot have every row of the intersection form nonnegative. This excludes affine configurations whose intersection matrix has a positive kernel vector.

theorem TauCeti.NumericalType.not_forall_sum_intersection_mul_nonneg_of_pos (T : NumericalType) {t : ℕ} {c : ℕ → T.Component} (hinj : ∀ i < t, ∀ j < t, c i = c j → i = j) (hcard : t < Fintype.card T.Component) {y : ℕ → ℤ} (hy : ∀ i < t, 0 ≤ y i) (hypos : ∃ i < t, 0 < y i) : ¬∀ i < t, 0 ≤ ∑ j ∈ Finset.range t, T.intersection (c i) (c j) * y j

A nonnegative, nonzero integral vector on a proper family of distinct components indexed by an initial segment of the natural numbers cannot have every row of the intersection form nonnegative.

Two components

theorem TauCeti.NumericalType.intersection_sq_lt_intersection_mul_intersection (T : NumericalType) (hcard : 2 < Fintype.card T.Component) {i j : T.Component} (hij : i ≠ j) : T.intersection i j ^ 2 < T.intersection i i * T.intersection j j

In a numerical type with more than two components, the intersection numbers of two distinct components satisfy aᵢⱼ² < aᵢᵢ aⱼⱼ: the principal 2 × 2 submatrix on {i, j} is negative definite.

Three components

theorem TauCeti.NumericalType.intersection_det_triple_neg (T : NumericalType) (hcard : 3 < Fintype.card T.Component) {i j k : T.Component} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : T.intersection i i * T.intersection j j * T.intersection k k - T.intersection i i * T.intersection j k ^ 2 - T.intersection j j * T.intersection i k ^ 2 - T.intersection k k * T.intersection i j ^ 2 + 2 * T.intersection i j * T.intersection i k * T.intersection j k < 0

In a numerical type with more than three components, the principal 3 × 3 submatrix of the intersection matrix on three distinct components i, j, k is negative definite, so its determinant aᵢᵢaⱼⱼaₖₖ - aᵢᵢaⱼₖ² - aⱼⱼaᵢₖ² - aₖₖaᵢⱼ² + 2aᵢⱼaᵢₖaⱼₖ, written out on the left below, is negative.

Four components

theorem TauCeti.NumericalType.intersection_det_four_pos (T : NumericalType) (hcard : 4 < Fintype.card T.Component) {i j k l : T.Component} (hij : i ≠ j) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) (hkl : k ≠ l) : 0 < T.intersection i i * T.intersection j j * T.intersection k k * T.intersection l l - T.intersection i i * T.intersection j j * T.intersection k l ^ 2 - T.intersection i i * T.intersection k k * T.intersection j l ^ 2 - T.intersection i i * T.intersection l l * T.intersection j k ^ 2 + 2 * T.intersection i i * T.intersection j k * T.intersection j l * T.intersection k l - T.intersection j j * T.intersection k k * T.intersection i l ^ 2 - T.intersection j j * T.intersection l l * T.intersection i k ^ 2 + 2 * T.intersection j j * T.intersection i k * T.intersection i l * T.intersection k l - T.intersection k k * T.intersection l l * T.intersection i j ^ 2 + 2 * T.intersection k k * T.intersection i j * T.intersection i l * T.intersection j l + 2 * T.intersection l l * T.intersection i j * T.intersection i k * T.intersection j k + T.intersection i j ^ 2 * T.intersection k l ^ 2 - 2 * T.intersection i j * T.intersection i k * T.intersection j l * T.intersection k l - 2 * T.intersection i j * T.intersection i l * T.intersection j k * T.intersection k l + T.intersection i k ^ 2 * T.intersection j l ^ 2 - 2 * T.intersection i k * T.intersection i l * T.intersection j k * T.intersection j l + T.intersection i l ^ 2 * T.intersection j k ^ 2

In a numerical type with more than four components, the principal 4 × 4 submatrix of the intersection matrix on four distinct components i, j, k, l is negative definite, so its determinant is positive. The displayed expression is the determinant written in terms of the ten entries on and above the diagonal.

Five components

theorem TauCeti.NumericalType.intersection_five_neg (T : NumericalType) (hcard : 5 < Fintype.card T.Component) {c₁ c₂ c₃ c₄ c₅ : T.Component} (h₁₂ : c₁ ≠ c₂) (h₁₃ : c₁ ≠ c₃) (h₁₄ : c₁ ≠ c₄) (h₁₅ : c₁ ≠ c₅) (h₂₃ : c₂ ≠ c₃) (h₂₄ : c₂ ≠ c₄) (h₂₅ : c₂ ≠ c₅) (h₃₄ : c₃ ≠ c₄) (h₃₅ : c₃ ≠ c₅) (h₄₅ : c₄ ≠ c₅) {y₁ y₂ y₃ y₄ y₅ : ℤ} (hy : ¬(y₁ = 0 ∧ y₂ = 0 ∧ y₃ = 0 ∧ y₄ = 0 ∧ y₅ = 0)) : T.intersection c₁ c₁ * y₁ ^ 2 + T.intersection c₂ c₂ * y₂ ^ 2 + T.intersection c₃ c₃ * y₃ ^ 2 + T.intersection c₄ c₄ * y₄ ^ 2 + T.intersection c₅ c₅ * y₅ ^ 2 + 2 * (T.intersection c₁ c₂ * y₁ * y₂ + T.intersection c₁ c₃ * y₁ * y₃ + T.intersection c₁ c₄ * y₁ * y₄ + T.intersection c₁ c₅ * y₁ * y₅ + T.intersection c₂ c₃ * y₂ * y₃ + T.intersection c₂ c₄ * y₂ * y₄ + T.intersection c₂ c₅ * y₂ * y₅ + T.intersection c₃ c₄ * y₃ * y₄ + T.intersection c₃ c₅ * y₃ * y₅ + T.intersection c₄ c₅ * y₄ * y₅) < 0

In a numerical type with more than five components, the intersection form is negative definite on the vectors supported on five distinct components c₁, …, c₅: its value at the vector taking the values y₁, …, y₅ there and vanishing elsewhere, written out below, is negative unless all five values vanish.

Six components

theorem TauCeti.NumericalType.intersection_six_neg (T : NumericalType) (hcard : 6 < Fintype.card T.Component) {c₁ c₂ c₃ c₄ c₅ c₆ : T.Component} (h₁₂ : c₁ ≠ c₂) (h₁₃ : c₁ ≠ c₃) (h₁₄ : c₁ ≠ c₄) (h₁₅ : c₁ ≠ c₅) (h₁₆ : c₁ ≠ c₆) (h₂₃ : c₂ ≠ c₃) (h₂₄ : c₂ ≠ c₄) (h₂₅ : c₂ ≠ c₅) (h₂₆ : c₂ ≠ c₆) (h₃₄ : c₃ ≠ c₄) (h₃₅ : c₃ ≠ c₅) (h₃₆ : c₃ ≠ c₆) (h₄₅ : c₄ ≠ c₅) (h₄₆ : c₄ ≠ c₆) (h₅₆ : c₅ ≠ c₆) {y₁ y₂ y₃ y₄ y₅ y₆ : ℤ} (hy : ¬(y₁ = 0 ∧ y₂ = 0 ∧ y₃ = 0 ∧ y₄ = 0 ∧ y₅ = 0 ∧ y₆ = 0)) : T.intersection c₁ c₁ * y₁ ^ 2 + T.intersection c₂ c₂ * y₂ ^ 2 + T.intersection c₃ c₃ * y₃ ^ 2 + T.intersection c₄ c₄ * y₄ ^ 2 + T.intersection c₅ c₅ * y₅ ^ 2 + T.intersection c₆ c₆ * y₆ ^ 2 + 2 * (T.intersection c₁ c₂ * y₁ * y₂ + T.intersection c₁ c₃ * y₁ * y₃ + T.intersection c₁ c₄ * y₁ * y₄ + T.intersection c₁ c₅ * y₁ * y₅ + T.intersection c₁ c₆ * y₁ * y₆ + T.intersection c₂ c₃ * y₂ * y₃ + T.intersection c₂ c₄ * y₂ * y₄ + T.intersection c₂ c₅ * y₂ * y₅ + T.intersection c₂ c₆ * y₂ * y₆ + T.intersection c₃ c₄ * y₃ * y₄ + T.intersection c₃ c₅ * y₃ * y₅ + T.intersection c₃ c₆ * y₃ * y₆ + T.intersection c₄ c₅ * y₄ * y₅ + T.intersection c₄ c₆ * y₄ * y₆ + T.intersection c₅ c₆ * y₅ * y₆) < 0

In a numerical type with more than six components, the intersection form is negative definite on vectors supported on six distinct components.