Double-ended forks of (-2)-indices

A chain of (-2)-indices cannot have an additional leaf at both its second and its penultimate component while remaining a proper subgraph of a numerical type. The two fork classifications make every displayed edge simply laced and all component weights equal. The affine-D marks give zero row sums on the chain and nonnegative row sums on the two leaves; a possible extra intersection between the leaves only increases their row sums. This contradicts negative definiteness.

This is Stacks, Lemma 55.5.11. It is part of the classification of proper connected subgraphs of (-2)-indices used to bound the multiplicities of a minimal numerical type.

Main result

• TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.not_oppositeFork: a proper chain of length at least four cannot carry distinct fork leaves at both ends.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.not_oppositeFork {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} {left right : T.Component} (hr : T.IsSelfIntersectionMinusTwoFork t c right) (hl : T.IsSelfIntersectionMinusTwoFork t (fun (i : ℕ) => c (t - 1 - i)) left) (ht : 3 < t) (hcard : t + 2 < Fintype.card T.Component) : False

A chain of at least four (-2)-indices cannot have additional leaves meeting its second and penultimate components when the displayed components form a proper subset of the numerical type. The leaves are necessarily distinct, but they may intersect each other; the affine-D marks still give nonnegative row sums (Stacks, Lemma 55.5.11).