Forks of (-2)-indices of arbitrary length

A fork consists of a chain of at least three components of self-intersection -2w, together with a distinct extra component of self-intersection -2w meeting the component indexed by t - 2. The extra component meets no other component of the chain. When the numerical type has components outside the fork, every component in the fork has the same weight and the displayed intersections equal that weight. Together with the chain's no-chord theorem, this identifies the induced intersection graph with a simply-laced fork.

This is Stacks, Lemma 55.5.9. It is one of the families in the classification of proper connected subgraphs of (-2)-indices used to bound the multiplicities of a minimal numerical type. The chain-length-three and chain-length-four cases subsumed here are respectively Stacks, Lemma 55.5.4 and Stacks, Lemma 55.5.7.

Main results

• TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork: a chain of length at least three with a distinct extra component of self-intersection -2w meeting the component indexed by t - 2.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.branch_intersection_eq_zero: the extra component meets no other component of the chain, without a properness assumption.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.exists_weight_intersection_eq: the weights and intersections of a proper fork whose chain has length at least three are all the simply-laced ones.

structure TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork (T : NumericalType) (t : ℕ) (c : ℕ → T.Component) (branch : T.Component) extends T.IsSelfIntersectionMinusTwoChain t c : Prop

A chain c 0 - ... - c (t - 1) of at least three components of self-intersection -2w, together with a distinct extra component branch, also of self-intersection -2w, meeting c (t - 2). The no-extra-intersection theorem shows that branch is a leaf.

• injOn (i : ℕ) : i < t → ∀ j < t, c i = c j → i = j
• intersection_self (i : ℕ) : i < t → T.intersection (c i) (c i) = -(2 * ↑↑(T.weight (c i)))
• intersection_succ_pos (i : ℕ) : i + 1 < t → 0 < T.intersection (c i) (c (i + 1))
• two_lt : 2 < t

  The chain contains at least three components.

• branch_ne (i : ℕ) : i < t → branch ≠ c i

  The extra component is not one of the chain components.

• branch_intersection_self : T.intersection branch branch = -(2 * ↑↑(T.weight branch))

  The extra component has self-intersection -2w.

• branch_intersection_pos : 0 < T.intersection (c (t - 2)) branch

  The extra component meets the penultimate chain component.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.branch_intersection_eq_zero {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} {branch : T.Component} (hf : T.IsSelfIntersectionMinusTwoFork t c branch) {i : ℕ} (hi : i < t) (hne : i ≠ t - 2) : T.intersection (c i) branch = 0

The extra leaf of a fork whose chain has length at least three meets no chain component other than the one indexed by t - 2.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.exists_weight_intersection_eq {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} {branch : T.Component} (hf : T.IsSelfIntersectionMinusTwoFork t c branch) (hcard : t + 1 < Fintype.card T.Component) : ∃ (w : ℕ+), (∀ i < t, ↑↑(T.weight (c i)) = ↑↑w) ∧ ↑↑(T.weight branch) = ↑↑w ∧ (∀ (i : ℕ), i + 1 < t → T.intersection (c i) (c (i + 1)) = ↑↑w) ∧ T.intersection (c (t - 2)) branch = ↑↑w

A proper fork whose chain has length at least three is simply laced: all its component weights agree and each displayed intersection is that common weight. Together with TauCeti.NumericalType.IsSelfIntersectionMinusTwoFork.branch_intersection_eq_zero and TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_eq_zero, this is the full classification of Stacks, Lemma 55.5.9.