Exceptional configurations of (-2)-indices

This file continues the classification of connected proper subgraphs of (-2)-indices in a numerical type with the exceptional diagram E₇. A chain of six components with an extra leaf at its fourth component is simply laced: all seven weights and all six displayed intersections agree, and there are no other edges. This gives the weight and intersection part of Stacks, Lemma 55.5.13.

Extending the length-two arm of this diagram by one component produces the affine E₇ diagram. Its marks (1, 2, 3, 4, 3, 2, 1, 2) form a positive kernel vector for the displayed intersection matrix. Negative definiteness on a proper family of components therefore rules out this configuration, which is Stacks, Lemma 55.5.15.

Main results

• TauCeti.NumericalType.exists_weight_intersection_branch_seven_eq: the E₇ configuration is simply laced.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_branch_eq_zero: a distinct eighth (-2)-index cannot meet the middle component of the chain, excluding the affine E₇ configuration.

theorem TauCeti.NumericalType.exists_weight_intersection_branch_seven_eq (T : NumericalType) {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain 6 c) {branch : T.Component} (hbranch_ne : ∀ i < 6, branch ≠ c i) (hbranch_self : T.intersection branch branch = -(2 * ↑↑(T.weight branch))) (hbranch_pos : 0 < T.intersection (c 3) branch) : ∃ (w : ℕ+), (∀ i < 6, ↑↑(T.weight (c i)) = ↑↑w) ∧ ↑↑(T.weight branch) = ↑↑w ∧ (∀ (i : ℕ), i + 1 < 6 → T.intersection (c i) (c (i + 1)) = ↑↑w) ∧ T.intersection (c 3) branch = ↑↑w ∧ ∀ i < 6, i ≠ 3 → T.intersection (c i) branch = 0

A chain c₁ - c₂ - c₃ - c₄ - c₅ - c₆ of (-2)-indices, together with a seventh (-2)-index meeting c₄, is simply laced. Thus all seven weights agree, every displayed intersection is that common weight, and the seventh component meets no other component of the chain. Together with the chain's no-chord theorem, this gives the weight and intersection claims for the proper E₇ configuration in Stacks, Lemma 55.5.13.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_branch_eq_zero (T : NumericalType) {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain 7 c) (hcard : 8 < Fintype.card T.Component) {branch : T.Component} (hbranch_ne : ∀ i < 7, branch ≠ c i) (hbranch_self : T.intersection branch branch = -(2 * ↑↑(T.weight branch))) : T.intersection (c 3) branch = 0

A distinct eighth (-2)-index cannot meet the middle component of a chain of seven (-2)-indices when the numerical type has any further component. This excludes the affine E₇ diagram as a proper subgraph, as in Stacks, Lemma 55.5.15.