Branched chains of (-2)-indices in a numerical type

A (-2)-index of a numerical type is a component i with gᵢ = 0 and aᵢᵢ = -2wᵢ. The configurations that (-2)-indices can form inside a numerical type with strictly more components are of Dynkin-diagram shape. This file treats the six components obtained by attaching a branch to the middle of a chain of five,

c₁ - c₂ - c₃ - c₄ - c₅, with a branch c₆ at c₃,

that is, the diagram E₆. All six weights are equal, each of the five displayed intersection numbers equals that common weight, and every other intersection number vanishes (Stacks, Lemma 55.5.10).

The free end c₆ of the branch meets no seventh component of self-intersection -2w: adding one would lengthen the branch into the affine diagram of type E₆, whose intersection matrix is singular (Stacks, Lemma 55.5.12). The vector taking the value three at the trivalent component c₃, two at its three neighbours and one at the three ends spans the kernel, so the intersection form vanishes at it, which negative definiteness on the vectors supported on a proper subset of the components forbids.

Main results

• TauCeti.NumericalType.exists_weight_intersection_branch_six_eq: a chain of five (-2)-indices with a branch at its middle component is simply laced, with equal weights and no further edges.
• TauCeti.NumericalType.intersection_eq_zero_of_branch_six: the free end of that branch meets no seventh component of self-intersection -2w.

theorem TauCeti.NumericalType.exists_weight_intersection_branch_six_eq (T : NumericalType) (hcard : 6 < Fintype.card T.Component) {c₁ c₂ c₃ c₄ c₅ c₆ : T.Component} (h₁ : T.intersection c₁ c₁ = -(2 * ↑↑(T.weight c₁))) (h₂ : T.intersection c₂ c₂ = -(2 * ↑↑(T.weight c₂))) (h₃ : T.intersection c₃ c₃ = -(2 * ↑↑(T.weight c₃))) (h₄ : T.intersection c₄ c₄ = -(2 * ↑↑(T.weight c₄))) (h₅ : T.intersection c₅ c₅ = -(2 * ↑↑(T.weight c₅))) (h₆ : T.intersection c₆ c₆ = -(2 * ↑↑(T.weight 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₆) (e₁₂ : 0 < T.intersection c₁ c₂) (e₂₃ : 0 < T.intersection c₂ c₃) (e₃₄ : 0 < T.intersection c₃ c₄) (e₄₅ : 0 < T.intersection c₄ c₅) (e₃₆ : 0 < T.intersection c₃ c₆) : ∃ (w : ℕ+), ↑↑(T.weight c₁) = ↑↑w ∧ ↑↑(T.weight c₂) = ↑↑w ∧ ↑↑(T.weight c₃) = ↑↑w ∧ ↑↑(T.weight c₄) = ↑↑w ∧ ↑↑(T.weight c₅) = ↑↑w ∧ ↑↑(T.weight c₆) = ↑↑w ∧ T.intersection c₁ c₂ = ↑↑w ∧ T.intersection c₂ c₃ = ↑↑w ∧ T.intersection c₃ c₄ = ↑↑w ∧ T.intersection c₄ c₅ = ↑↑w ∧ T.intersection c₃ c₆ = ↑↑w ∧ T.intersection c₁ c₃ = 0 ∧ T.intersection c₁ c₄ = 0 ∧ T.intersection c₁ c₅ = 0 ∧ T.intersection c₁ c₆ = 0 ∧ T.intersection c₂ c₄ = 0 ∧ T.intersection c₂ c₅ = 0 ∧ T.intersection c₂ c₆ = 0 ∧ T.intersection c₃ c₅ = 0 ∧ T.intersection c₄ c₆ = 0 ∧ T.intersection c₅ c₆ = 0

Six components of self-intersection -2w in a numerical type with more than six components forming the branched chain

c₁ - c₂ - c₃ - c₄ - c₅, with a branch c₆ at c₃,

all have the same weight, every displayed intersection equals that weight, and every other intersection vanishes. This is the classification of Stacks, Lemma 55.5.10.

theorem TauCeti.NumericalType.intersection_eq_zero_of_branch_six (T : NumericalType) (hcard : 7 < Fintype.card T.Component) {c₁ c₂ c₃ c₄ c₅ c₆ c₇ : T.Component} (h₁ : T.intersection c₁ c₁ = -(2 * ↑↑(T.weight c₁))) (h₂ : T.intersection c₂ c₂ = -(2 * ↑↑(T.weight c₂))) (h₃ : T.intersection c₃ c₃ = -(2 * ↑↑(T.weight c₃))) (h₄ : T.intersection c₄ c₄ = -(2 * ↑↑(T.weight c₄))) (h₅ : T.intersection c₅ c₅ = -(2 * ↑↑(T.weight c₅))) (h₆ : T.intersection c₆ c₆ = -(2 * ↑↑(T.weight c₆))) (h₇ : T.intersection c₇ c₇ = -(2 * ↑↑(T.weight 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₆) (h₅₇ : c₅ ≠ c₇) (h₆₇ : c₆ ≠ c₇) (e₁₂ : 0 < T.intersection c₁ c₂) (e₂₃ : 0 < T.intersection c₂ c₃) (e₃₄ : 0 < T.intersection c₃ c₄) (e₄₅ : 0 < T.intersection c₄ c₅) (e₃₆ : 0 < T.intersection c₃ c₆) : T.intersection c₆ c₇ = 0

The free end c₆ of the branched chain

c₁ - c₂ - c₃ - c₄ - c₅, with a branch c₆ at c₃,

of components of self-intersection -2w meets no seventh component of self-intersection -2w, in a numerical type with more than seven components. In particular a chain of five (-2)-indices with a leg of length two at its middle component does not occur as a proper subgraph (Stacks, Lemma 55.5.12).