Exceptional E₈ configurations of (-2)-indices

This file treats finite and affine E₈ configurations of (-2)-indices occurring in the classification of connected proper subgraphs of a numerical type. A chain of seven components with an extra leaf at its fifth component is simply laced: all eight weights and all seven displayed intersections agree, and there are no other edges. This is Stacks, Lemma 55.5.14.

Extending the long arm by one component produces the affine E₈ diagram. Its marks 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.16.

Main results

• IsSelfIntersectionMinusTwoChain.exists_weight_intersection_branch_eight_eq: the finite E₈ configuration is simply laced.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.not_affineE8: the affine E₈ configuration cannot be a proper subgraph of (-2)-indices.

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

A chain c₀ - c₁ - ⋯ - c₆ of (-2)-indices, together with an eighth (-2)-index meeting c₄, is simply laced. Thus all eight weights agree, every displayed intersection is that common weight, and the eighth component meets no other component of the chain. This gives the classification of the E₈ configuration in Stacks, Lemma 55.5.14.

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

The affine E₈ diagram cannot occur as a proper subgraph of (-2)-indices. Concretely, a chain of eight (-2)-indices cannot have a distinct ninth (-2)-index meeting the component c₅ when the numerical type has any further component. This is Stacks, Lemma 55.5.16.