Chains of (-2)-indices of arbitrary length

A (-2)-index of a numerical type is a component i with gᵢ = 0 and aᵢᵢ = -2wᵢ. The configurations that a set of (-2)-indices can form inside a numerical type with strictly more components are of Dynkin-diagram shape, and TauCeti/AlgebraicGeometry/Curves/StableReduction/NumericalType/ProperSubgraph.lean classifies those on at most six components. This file treats the one infinite family, a chain i₁ - i₂ - ⋯ - i_t of any length, packaged as TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.

The underlying adjacency graph of such a chain in a numerical type with more components is a path: no two of its components meet except along the chain, so in particular the chain never closes up into a cycle. From five components on, it also has at most one nonsimple edge, and that edge is at an end: all its weights are equal except possibly at one end, where the weight may be the double or the half of the common weight, and every edge has intersection number the larger of the weights of its two endpoints by TauCeti.NumericalType.intersection_eq_max_weight. This is Stacks, Lemma 55.5.8, whose source statement is restricted to more than five components because the five-component case is its Lemma 55.5.5.

Main results

• TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain: the predicate recording a chain of components of self-intersection -2w.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_eq_zero: two components of such a chain which are not consecutive do not meet, provided the numerical type has more components than the chain has length.
• TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.exists_weight_eq_except_one_end: the weights along such a chain of at least five components are constant except possibly at one end.

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

T.IsSelfIntersectionMinusTwoChain t c says that c 0, …, c (t - 1) are t distinct components of the numerical type T, each of self-intersection aᵢᵢ = -2wᵢ, in which consecutive components meet. Positions are indexed by ℕ, with only the values below t constrained, so that a block of consecutive positions is again a chain for the shifted index function.

This is weaker than asking each c i to be a TauCeti.NumericalType.IsMinusTwoIndex, which also requires gᵢ = 0: the genus plays no role in the classification of the configurations that (-2)-indices form, exactly as in the fixed-length classifications of Stacks, Section 0C7L already available.

• injOn (i : ℕ) : i < t → ∀ j < t, c i = c j → i = j

  The components of the chain are pairwise distinct.

• intersection_self (i : ℕ) : i < t → T.intersection (c i) (c i) = -(2 * ↑↑(T.weight (c i)))

  Every component of the chain has self-intersection -2w.

• intersection_succ_pos (i : ℕ) : i + 1 < t → 0 < T.intersection (c i) (c (i + 1))

  Consecutive components of the chain meet.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.ne {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {i j : ℕ} (hi : i < t) (hj : j < t) (hij : i ≠ j) : c i ≠ c j

Distinct positions of a chain carry distinct components.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_pos {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {i j : ℕ} (hij : j = i + 1) (hj : j < t) : 0 < T.intersection (c i) (c j)

Consecutive components of a chain meet, in the form in which the successor position is given by an equation rather than syntactically.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.mono {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {s : ℕ} (hs : s ≤ t) : T.IsSelfIntersectionMinusTwoChain s c

An initial block of a chain is again a chain.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.shift {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {r s : ℕ} (hrs : r + s ≤ t) : T.IsSelfIntersectionMinusTwoChain s fun (k : ℕ) => c (r + k)

Any block of consecutive positions of a chain is again a chain.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.injOn_snoc {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {branch : T.Component} (hbranch_ne : ∀ i < t, branch ≠ c i) (i : ℕ) : i < t + 1 → ∀ j < t + 1, ((if i = t then branch else c i) = if j = t then branch else c j) → i = j

A chain followed by a component outside the chain is injective on its first t + 1 terms.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.le_card_snoc {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {branch : T.Component} (hbranch_ne : ∀ i < t, branch ≠ c i) : t + 1 ≤ Fintype.card T.Component

A chain and a further distinct component contain at least t + 1 components.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.reverse {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) : T.IsSelfIntersectionMinusTwoChain t fun (i : ℕ) => c (t - 1 - i)

A chain read backwards is again a chain.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.cons {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) {x : T.Component} (hx_ne : ∀ i < t, x ≠ c i) (hx_self : T.intersection x x = -(2 * ↑↑(T.weight x))) (hx_pos : 0 < t → 0 < T.intersection x (c 0)) : T.IsSelfIntersectionMinusTwoChain (t + 1) fun (i : ℕ) => if i = 0 then x else c (i - 1)

Prepending a component of self-intersection -2w which is not in a chain and, when the chain is nonempty, meets its first component gives a chain one component longer.

@[simp]

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.card_image_range {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) : (Finset.image c (Finset.range t)).card = t

The components of a chain of length t form a set of t components.

theorem TauCeti.NumericalType.exists_chain_forall_le {T : NumericalType} (S : Finset T.Component) : ∃ (t : ℕ) (c : ℕ → T.Component), T.IsSelfIntersectionMinusTwoChain t c ∧ (∀ i < t, c i ∈ S) ∧ ∀ (t' : ℕ) (c' : ℕ → T.Component), T.IsSelfIntersectionMinusTwoChain t' c' → (∀ i < t', c' i ∈ S) → t' ≤ t

Every set of components contains a longest chain.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_eq_zero {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) {p q : ℕ} (hp : p < t) (hq : q < t) (hpq : p ≠ q) (hpq₁ : p + 1 ≠ q) (hqp₁ : q + 1 ≠ p) : T.intersection (c p) (c q) = 0

Two components of a chain of components of self-intersection -2w which are not consecutive in the chain do not meet, as soon as the numerical type has more components than the chain has length. In particular such a chain is never a cycle and has no chords: its underlying adjacency graph is a path. This is the graph-shape half of Stacks, Lemma 55.5.8.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.eq_of_intersection_pos {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t + 1 < Fintype.card T.Component) {x : T.Component} (hx_ne : ∀ i < t, x ≠ c i) (hx_self : T.intersection x x = -(2 * ↑↑(T.weight x))) {r s : ℕ} (hs : s < t) (hr : 0 < T.intersection (c r) x) (hrs : r ≤ s) (hsx : 0 < T.intersection (c s) x) : r = s

A component outside a chain meets at most one of its components, provided the numerical type has a component besides it and those of the chain: otherwise the chain would close up into a cycle.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_eq_ite {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} {w : ℤ} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) (hweight : ∀ i < t, ↑↑(T.weight (c i)) = w) (hedge : ∀ (i : ℕ), i + 1 < t → T.intersection (c i) (c (i + 1)) = w) {i j : ℕ} (hi : i < t) (hj : j < t) : T.intersection (c i) (c j) = if i = j then -(2 * w) else if i + 1 = j ∨ j + 1 = i then w else 0

The intersection entries of a proper simply laced chain with common weight w.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.left_sum_eq {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) (ht : 1 < t) (y : ℕ → ℤ) : ∑ j ∈ Finset.range t, T.intersection (c 0) (c j) * y j = T.intersection (c 0) (c 0) * y 0 + T.intersection (c 0) (c 1) * y 1

In a proper chain with at least two components, the left-end row of an intersection sum has only its diagonal and adjacent terms.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.interior_sum_eq {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) (y : ℕ → ℤ) {i : ℕ} (hi : 0 < i) (hit : i + 1 < t) : ∑ j ∈ Finset.range t, T.intersection (c i) (c j) * y j = T.intersection (c i) (c (i - 1)) * y (i - 1) + T.intersection (c i) (c i) * y i + T.intersection (c i) (c (i + 1)) * y (i + 1)

In a proper chain, an interior row of an intersection sum has only its two adjacent terms and its diagonal term.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.right_sum_eq {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) (ht : 1 < t) (y : ℕ → ℤ) : ∑ j ∈ Finset.range t, T.intersection (c (t - 1)) (c j) * y j = T.intersection (c (t - 1)) (c (t - 2)) * y (t - 2) + T.intersection (c (t - 1)) (c (t - 1)) * y (t - 1)

In a proper chain with at least two components, the right-end row of an intersection sum has only its diagonal and adjacent terms.

theorem TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.exists_weight_eq_except_one_end {T : NumericalType} {t : ℕ} {c : ℕ → T.Component} (hc : T.IsSelfIntersectionMinusTwoChain t c) (hcard : t < Fintype.card T.Component) (ht : 4 < t) : ∃ (W : ℤ), 0 < W ∧ (∀ (i : ℕ), 0 < i → i + 1 < t → ↑↑(T.weight (c i)) = W) ∧ (↑↑(T.weight (c 0)) = W ∨ ↑↑(T.weight (c 0)) = 2 * W ∨ 2 * ↑↑(T.weight (c 0)) = W) ∧ (↑↑(T.weight (c (t - 1))) = W ∨ ↑↑(T.weight (c (t - 1))) = 2 * W ∨ 2 * ↑↑(T.weight (c (t - 1))) = W) ∧ (↑↑(T.weight (c 0)) = W ∨ ↑↑(T.weight (c (t - 1))) = W)

The weights along a chain of components of self-intersection -2w in a numerical type with more components than the chain has length are constant except possibly at one end, where the weight may be twice or half the common interior weight. Together with TauCeti.NumericalType.IsSelfIntersectionMinusTwoChain.intersection_eq_zero and TauCeti.NumericalType.intersection_eq_max_weight, which turn these weights into the intersection numbers, this is Stacks, Lemma 55.5.8.