The double-edge bound for finite-type Cartan matrices

In a finite-type diagram an index carrying a multiple edge is joined to every other index by at most a single edge (TauCeti.IsFiniteType.apply_mul_apply_le_one_of_two_le) - a restriction on what is incident to one endpoint of the edge, not yet a count of the multiple edges of a whole diagram - and a triple edge is isolated outright (TauCeti.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three), which leaves G₂. A double edge is not isolated. Once the component carrying one has been shown to have no branch vertex - a step taken outside this file, as noted below - it is two chains, of p and of q vertices, joined at their last vertices by that edge, and that is the shape this file takes as given. Which of those survive is the chain half of the "chain/fork length constraints" of the Cartan--Killing classification, and, like the fork half in TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Basic, it is an arithmetic constraint:

2 p q < (p + 1) (q + 1),

equivalently (p - 1) (q - 1) < 2, whose solutions with both chains nonempty are q = 1 (the chains Cₙ), p = 1 (the chains Bₙ), and p = q = 2 (F₄).

This file builds that diagram as a matrix, TauCeti.doubleEdgeCartanMatrix, out of the chain entries of TauCeti.LinearAlgebra.RootSystem.Chain, and proves the bound. The elimination tool is the one the fork bound uses: 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). The certificate is the vector of marks TauCeti.doubleEdgeMark, which grows linearly along each of the two chains towards the double edge, in steps of q on the side of p vertices and of p + 1 on the other. Those two slopes are chosen so that the marks are annihilated at every vertex of the diagram except the far end of the second chain, where the row takes the value (p + 1) (q + 1) - 2 p q, which is ≤ 0 exactly when the bound fails.

The critical diagram, where the marks are a genuine null vector, is the extended Dynkin diagram F̃₄ = T(3, 2); it is recorded as a corollary. The bound is sharp along the two families it leaves: TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_right identifies the diagram at q = 1 with Mathlib's CartanMatrix.C (p + 1), so it really is of finite type there, and the case p = 1 follows by transposition.

The orientation is fixed once: the entry from the last vertex of the second chain to the last vertex of the first is -2, and the opposite entry is -1. The reversed diagram is the transpose (TauCeti.doubleEdgeCartanMatrix_transpose), which finite type is invariant under (TauCeti.IsFiniteType.transpose), and the bound is symmetric in p and q, so nothing is lost.

As with the fork bound, only the arithmetic constraint is proved here: the step that produces such a subdiagram from a finite-type diagram carrying a double edge - which is where the absence of a branch vertex is established - is outside this file.

Main definitions

• TauCeti.doubleEdgeCartanMatrix: the Cartan matrix of two chains, of p and of q vertices, joined by a double edge at their last vertices.
• TauCeti.doubleEdgeMark: the marks of that diagram, the test vector the bound is proved with.

Main results

• TauCeti.two_mul_mul_lt_succ_mul_succ_of_isFiniteType_doubleEdge and TauCeti.not_isFiniteType_doubleEdgeCartanMatrix_of_succ_mul_succ_le: the double-edge bound, 2 p q < (p + 1) (q + 1), and its contrapositive.
• TauCeti.eq_one_or_eq_one_or_eq_two_two_of_isFiniteType_doubleEdge: the admissible shapes. A double-edge diagram of finite type with nonempty chains has p = 1, or q = 1, or p = q = 2: the families Bₙ, Cₙ, and F₄.
• TauCeti.not_isFiniteType_affineF₄: the critical diagram is not of finite type.
• TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_right and TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_left: the two families the bound leaves are of finite type, so the bound is sharp and its hypothesis is not vacuous.

References

This file supplies the chain 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 (6), where the same linear weighting of the two chains gives (p - 1) (q - 1) < 2, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4.

The diagram and its marks

def TauCeti.doubleEdgeCartanMatrix (p q : ℕ) : Matrix (Fin p ⊕ Fin q) (Fin p ⊕ Fin q) ℤ

The Cartan matrix of a double-edge chain: two chains, of p and of q vertices, whose last vertices are joined by a double edge. The entry from the second chain to the first is -2 and the opposite entry is -1, so at q = 1 this is the Cartan matrix of type Cₚ₊₁ (TauCeti.doubleEdgeCartanMatrix_one_right).

Equations

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

@[simp]

theorem TauCeti.doubleEdgeCartanMatrix_inl_inl {p q : ℕ} (v w : Fin p) : doubleEdgeCartanMatrix p q (Sum.inl v) (Sum.inl w) = chainEntry ↑v ↑w

The first chain is a chain.

@[simp]

theorem TauCeti.doubleEdgeCartanMatrix_inr_inr {p q : ℕ} (v w : Fin q) : doubleEdgeCartanMatrix p q (Sum.inr v) (Sum.inr w) = chainEntry ↑v ↑w

The second chain is a chain.

@[simp]

theorem TauCeti.doubleEdgeCartanMatrix_inl_inr {p q : ℕ} (v : Fin p) (w : Fin q) : doubleEdgeCartanMatrix p q (Sum.inl v) (Sum.inr w) = if ↑v + 1 = p ∧ ↑w + 1 = q then -1 else 0

The two chains meet only at their last vertices, where the entry is -1 in this direction.

@[simp]

theorem TauCeti.doubleEdgeCartanMatrix_inr_inl {p q : ℕ} (v : Fin q) (w : Fin p) : doubleEdgeCartanMatrix p q (Sum.inr v) (Sum.inl w) = if ↑v + 1 = q ∧ ↑w + 1 = p then -2 else 0

The two chains meet only at their last vertices, where the entry is -2 in this direction.

@[simp]

theorem TauCeti.doubleEdgeCartanMatrix_transpose (p q : ℕ) : (doubleEdgeCartanMatrix p q).transpose = (doubleEdgeCartanMatrix q p).submatrix Sum.swap Sum.swap

Reversing the double edge transposes the matrix. The two orientations of the double edge give transposed diagrams, which is exactly the relation between Bₙ and Cₙ; since finite type is invariant under transposition (TauCeti.IsFiniteType.transpose), one orientation carries all the information.

def TauCeti.doubleEdgeMark (p q : ℕ) : Fin p ⊕ Fin q → ℚ

The marks of a double-edge chain: the value s + 1 at the vertex s of the first chain, scaled by q, and the value t + 1 at the vertex t of the second chain, scaled by p + 1. Both grow linearly towards the double edge, and the two slopes are in the ratio the double edge asks for.

In the critical case p = 3, q = 2 they are 2, 4, 6 along the first chain and 4, 8 along the second, that is, twice the marks 1, 2, 3, 4, 2 of the extended Dynkin diagram F̃₄ read along the diagram; the same formula serves in general, since the matrix annihilates them everywhere except at the far end of the second chain, whatever p and q are.

Equations

• TauCeti.doubleEdgeMark p q (Sum.inl v) = (↑↑v + 1) * ↑q
• TauCeti.doubleEdgeMark p q (Sum.inr w) = (↑↑w + 1) * (↑p + 1)

@[simp]

theorem TauCeti.doubleEdgeMark_inl {p q : ℕ} (v : Fin p) : doubleEdgeMark p q (Sum.inl v) = (↑↑v + 1) * ↑q

@[simp]

theorem TauCeti.doubleEdgeMark_inr {p q : ℕ} (w : Fin q) : doubleEdgeMark p q (Sum.inr w) = (↑↑w + 1) * (↑p + 1)

The rows of the diagram at its marks

Two computations, one for each kind of vertex. A chain annihilates a weight that is linear in the position away from its two ends, and the far end of the first chain is cancelled by the double edge; only the far end of the second chain is left, and there the bound is read off.

theorem TauCeti.sum_doubleEdgeCartanMatrix_mul_doubleEdgeMark_inl_eq_zero {p q : ℕ} (v : Fin p) : ∑ w : Fin p ⊕ Fin q, ↑(doubleEdgeCartanMatrix p q (Sum.inl v) w) * doubleEdgeMark p q w = 0

The rows at the first chain annihilate the marks. Away from the double edge this is the second difference of a linear weight; at the double edge the first chain contributes (p + 1) q and the double edge subtracts the same amount, which is what fixes the ratio of the two slopes.

theorem TauCeti.sum_doubleEdgeCartanMatrix_mul_doubleEdgeMark_inr {p q : ℕ} (w : Fin q) : ∑ u : Fin p ⊕ Fin q, ↑(doubleEdgeCartanMatrix p q (Sum.inr w) u) * doubleEdgeMark p q u = if ↑w + 1 = q then (↑p + 1) * (↑q + 1) - 2 * ↑p * ↑q else 0

The rows at the second chain annihilate the marks away from the double edge, and at the double edge they take the value the bound is read off: (p + 1) (q + 1) - 2 p q.

The bound

theorem TauCeti.two_mul_mul_lt_succ_mul_succ_of_isFiniteType_doubleEdge {p q : ℕ} (h : IsFiniteType (doubleEdgeCartanMatrix p q)) : 2 * p * q < (p + 1) * (q + 1)

The double-edge bound. Two chains of p and q vertices joined by a double edge form a diagram of finite type only if 2 p q < (p + 1) (q + 1), that is, only if (p - 1) (q - 1) < 2.

theorem TauCeti.not_isFiniteType_doubleEdgeCartanMatrix_of_succ_mul_succ_le {p q : ℕ} (h : (p + 1) * (q + 1) ≤ 2 * p * q) : ¬IsFiniteType (doubleEdgeCartanMatrix p q)

The contrapositive of TauCeti.two_mul_mul_lt_succ_mul_succ_of_isFiniteType_doubleEdge: a double-edge diagram violating the bound is not of finite type.

This is the shape the classification consumes. A candidate diagram is excluded by exhibiting an embedded double-edge chain with (p + 1) (q + 1) ≤ 2 p q, that is, by TauCeti.IsFiniteType.submatrix along an injection e with A.submatrix e e = doubleEdgeCartanMatrix p q.

theorem TauCeti.eq_one_or_eq_one_or_eq_two_two_of_isFiniteType_doubleEdge {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (h : IsFiniteType (doubleEdgeCartanMatrix p q)) : q = 1 ∨ p = 1 ∨ p = 2 ∧ q = 2

The admissible double-edge shapes. A double-edge diagram of finite type whose two chains are nonempty has one vertex on the second chain (the family Cₙ), or one vertex on the first (the family Bₙ), or two on each (F₄).

This is the exclusion half of the classification of the diagrams with a double edge. The converse, that these shapes are the diagrams of actual root systems, is the separate realization target of the same layer. That the two families are at least of finite type is TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_right and TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_left; the remaining shape, TauCeti.doubleEdgeCartanMatrix 2 2, is the diagram of F₄, but nothing here identifies it with TauCeti.DynkinType.F4.cartanMatrix, so its finite type is not established in this file.

theorem TauCeti.not_isFiniteType_affineF₄ : ¬IsFiniteType (doubleEdgeCartanMatrix 3 2)

The extended Dynkin diagram F̃₄, two chains of three and of two vertices joined by a double edge, is not of finite type.

Sharpness: the two families the bound leaves

The bound excludes everything outside Bₙ, Cₙ and F₄. That the two families do occur is proved here, by identifying the diagram at q = 1 with Mathlib's CartanMatrix.C. The third shape, TauCeti.doubleEdgeCartanMatrix 2 2, is left alone: the reindexing that identifies it with the canonical Cartan matrix of F₄ belongs to the assembly step of the classification, outside this file.

theorem TauCeti.doubleEdgeCartanMatrix_one_right (p : ℕ) : doubleEdgeCartanMatrix p 1 = (CartanMatrix.C (p + 1)).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv

A double-edge chain whose second chain is a single vertex is of type Cₙ. The n - 1 vertices of the first chain are the first n - 1 nodes of Cₙ, in order, and the lone vertex is the last node, at which the double edge of Cₙ points. That listing of the vertices in the order they occur along the diagram is Mathlib's canonical identification finSumFinEquiv.

theorem TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_right (p : ℕ) : IsFiniteType (doubleEdgeCartanMatrix p 1)

The double-edge diagrams with a single vertex on the second chain are of finite type: they are the family Cₙ.

theorem TauCeti.isFiniteType_doubleEdgeCartanMatrix_one_left (q : ℕ) : IsFiniteType (doubleEdgeCartanMatrix 1 q)

The double-edge diagrams with a single vertex on the first chain are of finite type: they are the family Bₙ, the transposes of the previous ones.