Connected proper sets of (-2)-indices

Let S be a set of components of a numerical type, each of self-intersection aᵢᵢ = -2wᵢ, which is connected, in the sense that no nonempty proper subset of S is disjoint from the rest of S, and which is a proper subset of the components. This file proves that the configuration formed by S has Dynkin-diagram shape (Stacks, Proposition 55.5.17): one of the following holds.

• S is the set of components of a chain c 0 - c 1 - ⋯ - c (t - 1) (TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain), the types A, B, C, F₄ and G₂.
• S is the set of components of a fork, a chain of at least three components together with a leaf meeting its penultimate component (TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork), the type D.
• S consists of a chain of five, six or seven components together with a leaf meeting the component c (t - 3) and no other component of the chain: the types E₆, E₇ and E₈.

Since the exceptional sets have at most eight elements, a connected proper set of at least nine such components is a chain or a fork. The weights and intersection numbers of each shape are determined by the classifications already available: IsSelfIntersectionMinusTwoChain.exists_weight_eq_except_one_end for chains, IsSelfIntersectionMinusTwoFork.exists_weight_intersection_eq for forks, and exists_weight_intersection_branch_six_eq, exists_weight_intersection_branch_seven_eq and IsSelfIntersectionMinusTwoChain.exists_weight_intersection_branch_eight_eq for the exceptional types. This is the input for the bound on the multiplicities of a minimal numerical type in Stacks, Lemma 55.7.3, where a maximal connected set of (-2)-indices is either small or a chain or a fork, the two shapes treated in TauCeti/AlgebraicGeometry/Curves/StableReduction/NumericalType/MultiplicityBound.lean.

Main results

• TauCeti.NumericalType.exists_chain_or_fork_or_exceptional: the classification above.

theorem TauCeti.NumericalType.exists_chain_or_fork_or_exceptional {T : NumericalType} {S : Finset T.Component} (hS : ∀ i ∈ S, T.intersection i i = -(2 * ↑↑(T.weight i))) (hcard : S.card < Fintype.card T.Component) (hconn : ∀ A ⊆ S, A.Nonempty → A ≠ S → ∃ i ∈ A, ∃ j ∈ S, j ∉ A ∧ 0 < T.intersection i j) : (∃ (t : ℕ) (c : ℕ → T.Component), T.IsSelfIntersectionMinusTwoChain t c ∧ Finset.image c (Finset.range t) = S) ∨ (∃ (t : ℕ) (c : ℕ → T.Component) (b : T.Component), T.IsSelfIntersectionMinusTwoFork t c b ∧ insert b (Finset.image c (Finset.range t)) = S) ∨ ∃ (t : ℕ) (c : ℕ → T.Component) (b : T.Component), T.IsSelfIntersectionMinusTwoChain t c ∧ 5 ≤ t ∧ t ≤ 7 ∧ (∀ i < t, b ≠ c i) ∧ T.intersection b b = -(2 * ↑↑(T.weight b)) ∧ 0 < T.intersection (c (t - 3)) b ∧ (∀ i < t, i ≠ t - 3 → T.intersection (c i) b = 0) ∧ insert b (Finset.image c (Finset.range t)) = S

Classification of connected proper sets of (-2)-indices. Let S be a proper subset of the components of a numerical type, each of self-intersection -2w, which is connected: every nonempty proper subset of S meets a component of S outside it. Then S is the set of components of a chain, or of a fork, or of a chain of five, six or seven components together with a leaf meeting c (t - 3) and no other component of the chain. These are the Dynkin diagrams of types A (with B, C, F₄ and G₂), D and E₆, E₇, E₈ (Stacks, Proposition 55.5.17).