A chain of a finite-type diagram carries at most one multiple edge

In a finite-type diagram the multiple edges at a single index are already restricted: an index carrying one is joined to every other index by at most a single edge (TauCeti.IsFiniteType.apply_mul_apply_le_one_of_two_le), and a triple edge is isolated outright (TauCeti.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three). Neither statement forbids two double edges lying at a distance from one another, and that is what this file rules out along a chain: if the first edge of a chain of m + 3 vertices is double, the last one is single.

The diagram to exclude is a chain whose two extreme edges are double, and there are two of them, because a Cartan matrix orients its multiple edges: writing the entry -2 of a double edge as an arrow, the two arrows either point away from each other towards the chain ends, or both the same way along the chain. On l + 1 vertices these are the diagrams of the affine Kac-Moody algebras D⁽²⁾ₗ₊₁ and A⁽²⁾₂ₗ, hence singular, so the certificate is in each case a genuine null vector: TauCeti.twoDoubleEdgeMark, which is 1 at the first vertex, 2 at every interior vertex, and, at the last vertex, 1 when the arrows point outwards and 2 when they agree.

A Cartan matrix is read here as A i j = ⟨αᵢ, αⱼ^∨⟩, the transpose of Kac's convention, so it is the rows that annihilate this vector, and what its entries list are the dual labels of those two diagrams, 1, 2, …, 2, 1 and 1, 2, …, 2, 2 — equivalently the marks of the dual diagrams C⁽¹⁾ₗ and A⁽²⁾₂ₗ, the latter renumbered backwards, which is what the name records.

Unlike the fork bound of TauCeti.LinearAlgebra.RootSystem.FiniteType.Star and the double-edge bound of TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge, which leave surviving shapes and so end in an arithmetic inequality, no member of this family is of finite type, whatever the length of the chain. That is what makes the conclusion available in the form the classification wants, TauCeti.IsFiniteType.apply_mul_apply_le_one_of_chain_of_two_le: a statement about an arbitrary finite-type matrix rather than about the model diagram. Its hypotheses are the data of a chain of indices carrying a multiple edge at one end - distinct indices, non-consecutive ones not joined, the interior edges, those joining the vertices s and s + 1 for 0 < s < m + 1, single, and the first edge multiple - and its conclusion is that the last edge is then single. That is exactly what a path in the diagram of the matrix supplies, and the extraction of such a path from a diagram carrying two double edges is the step left outside this file.

Note that the ends of the chain need not be the ends of the diagram: the hypotheses say nothing about indices outside the chain, since finite type passes to principal submatrices (TauCeti.IsFiniteType.submatrix).

Main definitions

• TauCeti.twoDoubleEdgeCartanMatrix: the Cartan matrix of a chain of m + 3 vertices whose first and last edges are double, the boolean argument orienting the last one.
• TauCeti.twoDoubleEdgeMark: the dual labels of that diagram, the null vector the exclusion is proved with.

Main results

• TauCeti.sum_twoDoubleEdgeCartanMatrix_mul_twoDoubleEdgeMark_eq_zero: the marks are a null vector of the diagram.
• TauCeti.not_isFiniteType_twoDoubleEdgeCartanMatrix: no doubly ended chain is of finite type, in either orientation and at every length.
• TauCeti.IsFiniteType.apply_mul_apply_le_one_of_chain_of_two_le: at most one edge of a chain of a finite-type diagram is multiple, the form the classification consumes.

References

This file supplies the "at most one multiple edge" 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 (5), and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4. The two affine diagrams and their labels are Table Aff 2 of V. G. Kac, Infinite Dimensional Lie Algebras, CUP (1990), whose convention aᵢⱼ = ⟨αⱼ, αᵢ^∨⟩ is the transpose of the one used here.

The doubly ended chain and its marks

def TauCeti.twoDoubleEdgeCartanMatrix (m : ℕ) (b : Bool) : Matrix (Fin (m + 3)) (Fin (m + 3)) ℤ

The Cartan matrix of a doubly ended chain: m + 3 vertices in a row, joined by single edges except for the first and the last edges, which are double.

The first double edge is oriented once and for all, the entry from the second vertex to the first being -2. The boolean b orients the last one: the entry from the vertex m + 1 to the vertex m + 2 is -2 when b is true, so that the two double edges point away from each other towards the chain ends, and the opposite entry is -2 when b is false, so that they point the same way along the chain. In the notation of Kac's tables, read through the transpose, the first diagram is D⁽²⁾ₘ₊₃ and the second is A⁽²⁾₂ₘ₊₄.

theorem TauCeti.twoDoubleEdgeCartanMatrix_def {m : ℕ} {b : Bool} (i j : Fin (m + 3)) : twoDoubleEdgeCartanMatrix m b i j = if ↑i = 1 ∧ ↑j = 0 then -2 else if ↑i = m + 1 ∧ ↑j = m + 2 then if b = true then -2 else -1 else if ↑i = m + 2 ∧ ↑j = m + 1 then if b = true then -1 else -2 else chainEntry ↑i ↑j

@[simp]

theorem TauCeti.twoDoubleEdgeCartanMatrix_one_zero {m : ℕ} {b : Bool} : twoDoubleEdgeCartanMatrix m b 1 0 = -2

The entry of the first double edge that carries the arrow.

@[simp]

theorem TauCeti.twoDoubleEdgeCartanMatrix_zero_one {m : ℕ} {b : Bool} : twoDoubleEdgeCartanMatrix m b 0 1 = -1

The opposite entry of the first double edge.

@[simp]

theorem TauCeti.twoDoubleEdgeCartanMatrix_last_left {m : ℕ} {b : Bool} : twoDoubleEdgeCartanMatrix m b ⟨m + 1, ⋯⟩ ⟨m + 2, ⋯⟩ = if b = true then -2 else -1

The entry of the last double edge, from the vertex m + 1 to the vertex m + 2.

@[simp]

theorem TauCeti.twoDoubleEdgeCartanMatrix_last_right {m : ℕ} {b : Bool} : twoDoubleEdgeCartanMatrix m b ⟨m + 2, ⋯⟩ ⟨m + 1, ⋯⟩ = if b = true then -1 else -2

The entry of the last double edge, from the vertex m + 2 to the vertex m + 1.

def TauCeti.twoDoubleEdgeMark (m : ℕ) (b : Bool) (s : Fin (m + 3)) : ℚ

The marks of a doubly ended chain: 1 at the first vertex, 2 at every other one, except that the last vertex also carries 1 when the two double edges point outwards towards the chain ends.

At the vertices of the chain these are the dual labels of the affine diagram the chain is, the marks of its dual: 1, 2, …, 2, 1 for D⁽²⁾ₘ₊₃, when b is true, and 1, 2, …, 2, 2 for A⁽²⁾₂ₘ₊₄, when b is false. It is the dual labels, and so the rows of the matrix, that occur here because the convention of this repository, A i j = ⟨αᵢ, αⱼ^∨⟩, is the transpose of Kac's. The function is indexed by the vertices Fin (m + 3) of the diagram.

theorem TauCeti.twoDoubleEdgeMark_def {m : ℕ} {b : Bool} (s : Fin (m + 3)) : twoDoubleEdgeMark m b s = if ↑s = 0 ∨ b = true ∧ ↑s = m + 2 then 1 else 2

@[simp]

theorem TauCeti.twoDoubleEdgeMark_zero {m : ℕ} {b : Bool} : twoDoubleEdgeMark m b 0 = 1

The first vertex of the chain carries the mark 1.

@[simp]

theorem TauCeti.twoDoubleEdgeMark_last {m : ℕ} {b : Bool} : twoDoubleEdgeMark m b ⟨m + 2, ⋯⟩ = if b = true then 1 else 2

The last vertex carries the mark 1 exactly when the double edges point outwards.

@[simp]

theorem TauCeti.twoDoubleEdgeMark_interior {m : ℕ} {b : Bool} (s : Fin (m + 3)) (hzero : 0 < ↑s) (hlast : ↑s < m + 2) : twoDoubleEdgeMark m b s = 2

Every vertex strictly between the two ends carries the mark 2.

theorem TauCeti.twoDoubleEdgeMark_pos {m : ℕ} {b : Bool} (s : Fin (m + 3)) : 0 < twoDoubleEdgeMark m b s

The marks are positive, which is what makes them a nonzero certificate.

The rows of the diagram at its marks

theorem TauCeti.sum_twoDoubleEdgeCartanMatrix_mul_twoDoubleEdgeMark_eq_zero {m : ℕ} {b : Bool} (i : Fin (m + 3)) : ∑ j : Fin (m + 3), ↑(twoDoubleEdgeCartanMatrix m b i j) * twoDoubleEdgeMark m b j = 0

The marks are a null vector of the doubly ended chain: every row annihilates them.

theorem TauCeti.not_isFiniteType_twoDoubleEdgeCartanMatrix (m : ℕ) (b : Bool) : ¬IsFiniteType (twoDoubleEdgeCartanMatrix m b)

No doubly ended chain is of finite type: whatever the length of the chain, and whichever way the two double edges are oriented, the marks are a nonzero null vector, and a finite-type matrix admits none.

Together with TauCeti.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three, which isolates a triple edge, this is the whole of the "at most one multiple edge" step of the classification: it is turned into a statement about an arbitrary finite-type matrix in TauCeti.IsFiniteType.apply_mul_apply_le_one_of_chain_of_two_le.

The shortest doubly ended chains

The two diagrams on three vertices, written out; they fix the conventions. They are also the two diagrams that the classical argument reaches by contracting the chain between the two double edges, a contraction that is not needed here, since the marks are available at every length.

theorem TauCeti.twoDoubleEdgeCartanMatrix_zero_true : twoDoubleEdgeCartanMatrix 0 true = !![2, -1, 0; -2, 2, -2; 0, -1, 2]

The shortest doubly ended chain with the two double edges pointing outwards towards the chain ends: the twisted affine diagram D⁽²⁾₃, whose dual labels are 1, 2, 1.

theorem TauCeti.twoDoubleEdgeCartanMatrix_zero_false : twoDoubleEdgeCartanMatrix 0 false = !![2, -1, 0; -2, 2, -1; 0, -2, 2]

The shortest doubly ended chain with the two double edges pointing the same way: the twisted affine diagram A⁽²⁾₄, whose dual labels are 1, 2, 2.

Two double edges along a chain of an arbitrary diagram

theorem TauCeti.IsFiniteType.apply_mul_apply_le_one_of_chain_of_two_le {m : ℕ} {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) {v : ℕ → B} (hv : Set.InjOn v (Set.Iio (m + 3))) (hzero : ∀ (s t : ℕ), s + 1 < t → t < m + 3 → A (v s) (v t) = 0) (hsimple : ∀ (s : ℕ), 0 < s → s < m + 1 → A (v s) (v (s + 1)) * A (v (s + 1)) (v s) = 1) (hfirst : 2 ≤ A (v 0) (v 1) * A (v 1) (v 0)) : A (v (m + 1)) (v (m + 2)) * A (v (m + 2)) (v (m + 1)) ≤ 1

At most one edge of a chain of a finite-type diagram is multiple. Let v 0, …, v (m + 2) be distinct indices of a finite-type matrix, non-consecutive ones not joined at all and the interior edges of the chain - those joining v s to v (s + 1) for 0 < s < m + 1 - single. If the first edge, the one joining v 0 to v 1, is multiple, then the last one, joining v (m + 1) to v (m + 2), is single; nothing is assumed about that last edge beforehand.

Nothing is assumed about the indices outside the chain: finite type passes to principal submatrices, so the chain may sit anywhere inside a larger diagram. The hypotheses are what a path in the diagram of the matrix provides, the non-adjacency of non-consecutive vertices coming from the diagram of a finite-type matrix being a forest (TauCeti.isAcyclic_diagramGraph).