The fork bound for finite-type Cartan matrices

A connected finite-type diagram is a tree whose vertices have degree at most three. Such a tree may branch at several vertices, and a branch vertex together with a choice of path into each of its three branches carries a star: that vertex as the centre, with three arms hanging off it. Which stars survive is the fork half of the "chain/fork length constraints" of the Cartan-Killing classification, and it is an arithmetic constraint. Writing p, q, r for the numbers of vertices on the three arms counting the centre, a star of finite type satisfies

1 / p + 1 / q + 1 / r > 1,

whose solutions with p ≤ q ≤ r are (1, q, r), (2, 2, r), (2, 3, 3), (2, 3, 4) and (2, 3, 5) - the chains Aₙ, the forks Dₙ, and E₆, E₇, E₈.

Only that arithmetic constraint is proved here. The step that produces a star from a diagram with a branch vertex is outside this file, and so is the constraint governing a multiple edge (the one behind B, C, F₄), which is TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge.Basic.

This file builds the star as a matrix, TauCeti.starCartanMatrix, out of the chain entries of TauCeti.LinearAlgebra.RootSystem.Chain, over an arbitrary finite index type of arms, and proves the bound. The elimination tool is a new one, living with the others in TauCeti.LinearAlgebra.RootSystem.FiniteType.Basic: a finite-type matrix admits no nonzero subdominant vector, one whose every coordinate xᵢ has xᵢ · (A x)ᵢ ≤ 0 (TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos), because the symmetrized quadratic form evaluates at such a vector to ∑ᵢ dᵢ xᵢ (A x)ᵢ ≤ 0. The certificate for a star is its vector of marks TauCeti.starMark, which decreases linearly along each arm, from p q r at the centre down to q r at the far end of the first arm. The marks are annihilated by the matrix at every arm vertex, and at the centre they take the value qr + pr + pq - pqr, which is ≤ 0 exactly when the fork bound fails.

The three critical stars, where the marks are a genuine null vector, are the extended Dynkin diagrams Ẽ₆ = T(3, 3, 3), Ẽ₇ = T(2, 4, 4) and Ẽ₈ = T(2, 3, 6); they are recorded as corollaries. Since the argument is uniform in the number of arms, the n-armed form of the bound, ∑ᵢ 1 / pᵢ > n - 2, comes out at the same time, and at n = 4 with every pᵢ = 2 it reproves the exclusion of D̃₄ that TauCeti.not_isFiniteType_affineD₄ gets from the degree bound.

Main definitions

• TauCeti.StarIndex: the vertices of a star - a centre none, and ℓ i further vertices on the arm i, the vertex some ⟨i, t⟩ sitting at distance t + 1 from the centre.
• TauCeti.starCartanMatrix: the Cartan matrix of a star, simply laced by construction.
• TauCeti.starIndexCongrArms: the relabelling of the vertices of a star induced by a relabelling of its arms, under which both the Cartan matrix (TauCeti.starCartanMatrix_comp) and finite type (TauCeti.isFiniteType_starCartanMatrix_comp_iff) are invariant.
• TauCeti.starMark: the marks of a star, the test vector the bound is proved with.

Main results

• TauCeti.card_sub_two_lt_sum_inv_of_isFiniteType_star and TauCeti.not_isFiniteType_starCartanMatrix_of_sum_inv_le: the fork bound, ∑ᵢ 1 / (ℓ i + 1) > n - 2 for a star of finite type with n arms, and its contrapositive.
• TauCeti.one_lt_sum_inv_of_isFiniteType_star_three and TauCeti.not_isFiniteType_starCartanMatrix_three_of_sum_inv_le_one: the same pair for three arms, where the bound reads 1 / p + 1 / q + 1 / r > 1.
• TauCeti.eq_zero_or_eq_one_one_or_eq_one_two_le_four_of_isFiniteType_star_three: the admissible three-armed shapes. A finite-type star with arms of a ≤ b ≤ c further vertices has a = 0 (a chain), or a = b = 1 (a fork of type D), or a = 1, b = 2 and c ≤ 4 (types E₆, E₇, E₈). The solutions are read off Mathlib's ADEInequality.lt_three, .lt_four and .lt_six.
• TauCeti.not_isFiniteType_affineE₆, TauCeti.not_isFiniteType_affineE₇, TauCeti.not_isFiniteType_affineE₈: the three critical stars are not of finite type.

References

This file supplies the fork half of the "chain/fork length constraints" step of the classification of finite-type Cartan matrices, Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, step (7), where the inequality 1/p + 1/q + 1/r > 1 is obtained from the same linear weighting of the arms, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4.

@[reducible, inline]

abbrev TauCeti.StarIndex {α : Type u_1} (ℓ : α → ℕ) : Type u_1

The vertices of the star with arms of lengths ℓ: a centre, written none, together with ℓ i further vertices on the arm i, the vertex some ⟨i, t⟩ sitting at distance t + 1 from the centre. An arm with ℓ i = 0 is absent, so the degree of the centre is the number of i with ℓ i ≠ 0.

Equations

• TauCeti.StarIndex ℓ = Option ((i : α) × Fin (ℓ i))

def TauCeti.starCartanMatrix {α : Type u_1} [DecidableEq α] (ℓ : α → ℕ) : Matrix (StarIndex ℓ) (StarIndex ℓ) ℤ

The Cartan matrix of a star: the simply-laced matrix whose diagram is the star with arms of lengths ℓ. Two vertices are joined exactly when they are consecutive along a common arm, the centre counting as position 0 of every arm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.starCartanMatrix_none_none {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} : starCartanMatrix ℓ none none = 2

@[simp]

theorem TauCeti.starCartanMatrix_none_some {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} (w : (i : α) × Fin (ℓ i)) : starCartanMatrix ℓ none (some w) = if ↑w.snd = 0 then -1 else 0

The centre is joined precisely to the first vertex of each nonempty arm.

@[simp]

theorem TauCeti.starCartanMatrix_some_none {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} (v : (i : α) × Fin (ℓ i)) : starCartanMatrix ℓ (some v) none = if ↑v.snd = 0 then -1 else 0

The centre is joined precisely to the first vertex of each nonempty arm.

@[simp]

theorem TauCeti.starCartanMatrix_some_some {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} (v w : (i : α) × Fin (ℓ i)) : starCartanMatrix ℓ (some v) (some w) = if v.fst = w.fst then if ↑v.snd = ↑w.snd then 2 else if ↑v.snd = ↑w.snd + 1 then -1 else if ↑w.snd = ↑v.snd + 1 then -1 else 0 else 0

Two arm vertices have entry 2 when equal, -1 when consecutive on the same arm, and 0 otherwise.

@[simp]

theorem TauCeti.starCartanMatrix_transpose {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} : (starCartanMatrix ℓ).transpose = starCartanMatrix ℓ

A star is simply laced, in particular symmetric: each arm is a chain, and being on a common arm is a symmetric relation.

Relabelling the arms

def TauCeti.starIndexCongrArms {α : Type u_1} {β : Type u_2} (e : α ≃ β) (ℓ : β → ℕ) : StarIndex (ℓ ∘ ⇑e) ≃ StarIndex ℓ

Relabelling the arms of a star: an equivalence e : α ≃ β of arm indices carries the star with arms ℓ ∘ e isomorphically onto the star with arms ℓ, moving the vertex at position t of the arm i to the same position of the arm e i and fixing the centre.

Equations

• TauCeti.starIndexCongrArms e ℓ = e.sigmaCongrLeft.optionCongr

@[simp]

theorem TauCeti.starIndexCongrArms_none {α : Type u_1} {β : Type u_2} (e : α ≃ β) (ℓ : β → ℕ) : (starIndexCongrArms e ℓ) none = none

Relabelling the arms fixes the centre.

@[simp]

theorem TauCeti.starIndexCongrArms_some {α : Type u_1} {β : Type u_2} (e : α ≃ β) (ℓ : β → ℕ) (v : (i : α) × Fin (ℓ (e i))) : (starIndexCongrArms e ℓ) (some v) = some ⟨e v.fst, v.snd⟩

Relabelling the arms keeps each arm vertex at its position along its (renamed) arm.

@[simp]

theorem TauCeti.starCartanMatrix_comp_apply {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] (e : α ≃ β) (ℓ : β → ℕ) (v w : StarIndex (ℓ ∘ ⇑e)) : starCartanMatrix (ℓ ∘ ⇑e) v w = starCartanMatrix ℓ ((starIndexCongrArms e ℓ) v) ((starIndexCongrArms e ℓ) w)

Relabelling the arms does not change an entry of the Cartan matrix of a star.

theorem TauCeti.starCartanMatrix_comp {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] (e : α ≃ β) (ℓ : β → ℕ) : starCartanMatrix (ℓ ∘ ⇑e) = (starCartanMatrix ℓ).submatrix ⇑(starIndexCongrArms e ℓ) ⇑(starIndexCongrArms e ℓ)

Relabelling the arms reindexes the Cartan matrix of a star.

Deliberately not @[simp]: it replaces the compact starCartanMatrix (ℓ ∘ e) by a submatrix, so it would preempt the normalizations that strip the relabelling outright, such as TauCeti.isFiniteType_starCartanMatrix_comp_iff. The entrywise TauCeti.starCartanMatrix_comp_apply is the simp-normal form of a relabelled entry.

theorem TauCeti.isFiniteType_starCartanMatrix_comp {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] {m : β → ℕ} (e : α ≃ β) (h : IsFiniteType (starCartanMatrix m)) : IsFiniteType (starCartanMatrix (m ∘ ⇑e))

Finite type is invariant under a relabelling of the arms of a star.

@[simp]

theorem TauCeti.isFiniteType_starCartanMatrix_comp_iff {α : Type u_1} [DecidableEq α] {β : Type u_2} [DecidableEq β] [Fintype α] [Fintype β] {m : β → ℕ} (e : α ≃ β) : IsFiniteType (starCartanMatrix (m ∘ ⇑e)) ↔ IsFiniteType (starCartanMatrix m)

Finite type is invariant under a relabelling of the arms of a star, in either direction.

def TauCeti.starMark {α : Type u_1} [DecidableEq α] [Fintype α] (ℓ : α → ℕ) : StarIndex ℓ → ℚ

The marks of a star: the value ∏ᵢ (ℓ i + 1) at the centre, decreasing linearly along the arm i in steps of ∏_{j ≠ i} (ℓ j + 1), down to that step itself at the far end of the arm.

In the critical cases these are a positive multiple of the marks of the corresponding extended Dynkin diagram - for ℓ = ![2, 2, 2] they are 9 times the marks of Ẽ₆ - and the same formula serves in general: the Cartan matrix annihilates them at every arm vertex whatever the arm lengths are, and only the value at the centre feels the fork bound.

Equations

• TauCeti.starMark ℓ none = ∏ i : α, (↑(ℓ i) + 1)
• TauCeti.starMark ℓ (some v) = (↑(ℓ v.fst) - ↑↑v.snd) * ∏ j ∈ {v.fst}ᶜ, (↑(ℓ j) + 1)

@[simp]

theorem TauCeti.starMark_none {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] : starMark ℓ none = ∏ i : α, (↑(ℓ i) + 1)

@[simp]

theorem TauCeti.starMark_some {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] (v : (i : α) × Fin (ℓ i)) : starMark ℓ (some v) = (↑(ℓ v.fst) - ↑↑v.snd) * ∏ j ∈ {v.fst}ᶜ, (↑(ℓ j) + 1)

theorem TauCeti.starMark_pos {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] (v : StarIndex ℓ) : 0 < starMark ℓ v

The marks are positive: the centre carries the largest of them.

The rows of a star at its marks

The two computations behind the bound: the row of starCartanMatrix at an arm vertex annihilates the marks, and the row at the centre evaluates to ∑ᵢ ∏_{j ≠ i} (ℓ j + 1) - (n - 2) ∏ᵢ (ℓ i + 1). Both are assembled from the chain row of TauCeti.LinearAlgebra.RootSystem.Chain, TauCeti.sum_range_chainEntry_mul, taken at an abstract weight function g.

theorem TauCeti.sum_starCartanMatrix_mul_starMark_some_eq_zero {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] (v : (i : α) × Fin (ℓ i)) : ∑ w : StarIndex ℓ, ↑(starCartanMatrix ℓ (some v) w) * starMark ℓ w = 0

The rows of a star at an arm vertex annihilate the marks. The marks are linear along each arm, and the centre supplies exactly the value the linear function takes at position 0, so the three-term recurrence of a chain closes at both ends.

This is not a simp lemma, and neither is the companion TauCeti.sum_starCartanMatrix_mul_starMark_none: the left-hand side is not in simp-normal form. Fintype.sum_option splits the sum over TauCeti.StarIndex into the centre and the arms, and the entry lemmas above then rewrite the summands, so simp has dismantled the left-hand side before this equation could fire; the attribute reports only as a simpNF violation. Both rows are stated in the shape TauCeti.IsFiniteType.eq_zero_of_forall_mul_sum_apply_mul_nonpos consumes, and their call sites reach them by rw.

theorem TauCeti.sum_starCartanMatrix_mul_starMark_none {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] : ∑ w : StarIndex ℓ, ↑(starCartanMatrix ℓ none w) * starMark ℓ w = ∑ i : α, ∏ j ∈ {i}ᶜ, (↑(ℓ j) + 1) - (↑(Fintype.card α) - 2) * ∏ i : α, (↑(ℓ i) + 1)

The row of a star at the centre, evaluated at the marks. With n arms and pᵢ = ℓ i + 1 vertices on the arm i counting the centre, the value is ∑ᵢ ∏_{j ≠ i} pⱼ - (n - 2) ∏ᵢ pᵢ, that is, (∑ᵢ 1 / pᵢ - (n - 2)) ∏ᵢ pᵢ. This is the only place the shape of the star is felt.

Not a simp lemma, for the reason given at TauCeti.sum_starCartanMatrix_mul_starMark_some_eq_zero.

theorem TauCeti.card_sub_two_lt_sum_inv_of_isFiniteType_star {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] (h : IsFiniteType (starCartanMatrix ℓ)) : ↑(Fintype.card α) - 2 < ∑ i : α, (↑(ℓ i) + 1)⁻¹

The fork bound. A star of finite type with n arms carrying ℓ i vertices each, so pᵢ = ℓ i + 1 vertices counting the centre, satisfies ∑ᵢ 1 / pᵢ > n - 2.

For three arms this is 1 / p + 1 / q + 1 / r > 1, the inequality that leaves only the forks of types D and E; see TauCeti.eq_zero_or_eq_one_one_or_eq_one_two_le_four_of_isFiniteType_star_three.

theorem TauCeti.not_isFiniteType_starCartanMatrix_of_sum_inv_le {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} [Fintype α] (h : ∑ i : α, (↑(ℓ i) + 1)⁻¹ ≤ ↑(Fintype.card α) - 2) : ¬IsFiniteType (starCartanMatrix ℓ)

The contrapositive of TauCeti.card_sub_two_lt_sum_inv_of_isFiniteType_star: a star violating the fork bound is not of finite type.

This is the shape the classification consumes. A candidate diagram is excluded by exhibiting an embedded star with ∑ᵢ 1 / pᵢ ≤ n - 2, that is, by TauCeti.IsFiniteType.submatrix along an injection e with A.submatrix e e = starCartanMatrix ℓ.

The three-armed case

The classification meets the bound at a branch vertex, where there are exactly three arms and the inequality reads 1 / p + 1 / q + 1 / r > 1. Its solutions are the chains, the forks of type D, and the three exceptional shapes.

theorem TauCeti.one_lt_sum_inv_of_isFiniteType_star_three {a b c : ℕ} (h : IsFiniteType (starCartanMatrix ![a, b, c])) : 1 < (↑a + 1)⁻¹ + (↑b + 1)⁻¹ + (↑c + 1)⁻¹

The fork bound for three arms, 1 / p + 1 / q + 1 / r > 1.

theorem TauCeti.not_isFiniteType_starCartanMatrix_three_of_sum_inv_le_one {a b c : ℕ} (h : (↑a + 1)⁻¹ + (↑b + 1)⁻¹ + (↑c + 1)⁻¹ ≤ 1) : ¬IsFiniteType (starCartanMatrix ![a, b, c])

The contrapositive of TauCeti.one_lt_sum_inv_of_isFiniteType_star_three: a three-armed star with 1 / p + 1 / q + 1 / r ≤ 1 is not of finite type.

theorem TauCeti.eq_zero_or_eq_one_one_or_eq_one_two_le_four_of_isFiniteType_star_three {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) (h : IsFiniteType (starCartanMatrix ![a, b, c])) : a = 0 ∨ a = 1 ∧ b = 1 ∨ a = 1 ∧ b = 2 ∧ c ≤ 4

The admissible three-armed shapes. A star of finite type whose three arms carry a ≤ b ≤ c vertices besides the centre is a chain (a = 0), a fork of type D (a = b = 1), or one of E₆, E₇, E₈ (a = 1, b = 2 and c ≤ 4).

This is the exclusion half of the classification of forks. The converse, that each of these shapes is the diagram of an actual root system, is the separate realization target of the same layer and is not proved here.

theorem TauCeti.not_isFiniteType_affineE₆ : ¬IsFiniteType (starCartanMatrix ![2, 2, 2])

The extended Dynkin diagram Ẽ₆, the star with three arms of two vertices each, is not of finite type: its marks are a null vector.

theorem TauCeti.not_isFiniteType_affineE₇ : ¬IsFiniteType (starCartanMatrix ![1, 3, 3])

The extended Dynkin diagram Ẽ₇, the star with arms of one, three and three vertices, is not of finite type.

theorem TauCeti.not_isFiniteType_affineE₈ : ¬IsFiniteType (starCartanMatrix ![1, 2, 5])

The extended Dynkin diagram Ẽ₈, the star with arms of one, two and five vertices, is not of finite type.