Chains with simple or double edges

The diagrams that the classification of finite-type Cartan matrices has to weigh are built out of chains. This file isolates the entry functions for a simply-laced chain and for a chain whose last edge may be double, together with the summation identities used by weighting arguments.

The diagrams that carry the length constraints of the classification - the stars of TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Basic, the double-edge chains of TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge.Basic, and the forked double-edge diagrams of TauCeti.LinearAlgebra.RootSystem.FiniteType.ForkedDoubleEdge - are all assembled from chains and are all excluded by a vector that is linear along each chain they contain. The simply-laced entry function and row sum are the special case L = 0 of their type-B counterparts.

Main definitions

• TauCeti.chainEntry: the Cartan-matrix entry of a chain between two positions along it.
• TauCeti.chainBEntry: the Cartan-matrix entry of a chain whose last edge may be double.

Main results

• TauCeti.chainEntry_eq_cartanMatrix_A: a chain of n positions is Mathlib's Cartan matrix of type Aₙ, which is what makes the name of the entry function the right one.
• TauCeti.sum_range_chainEntry_mul: the row of a chain at a position, evaluated at a weight g. Away from the two ends it is the second difference 2 g (m + 1) - g m - g (m + 2), so a weight that is linear in the position is annihilated there.
• TauCeti.sum_range_chainEntry_mul_affine: the resulting formula for an affine weight.
• TauCeti.sum_range_chainBEntry_mul: the corresponding row sum with a double last edge.

References

The chain weighting is the calculation of J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4.

def TauCeti.chainBEntry (L s t : ℕ) : ℤ

The Cartan-matrix entry of a chain of type B between the positions s and t, the last position being L: 2 on the diagonal, -1 between consecutive positions, and -2 from the position before L to L itself, whose root is the short one.

A value of L outside the range of positions describes a simply-laced chain, of type A; L = 0 is the convenient such value, since no position is the successor of 0.

Equations

• TauCeti.chainBEntry L s t = if s = t then 2 else if s + 1 = t then if t = L then -2 else -1 else if t + 1 = s then -1 else 0

theorem TauCeti.chainBEntry_def (L s t : ℕ) : chainBEntry L s t = if s = t then 2 else if s + 1 = t then if t = L then -2 else -1 else if t + 1 = s then -1 else 0

The entries of a chain of type B, spelled out: this is how a file that has to case on all of them at once reaches the definition, whose body is not exposed.

@[simp]

theorem TauCeti.chainBEntry_self (L s : ℕ) : chainBEntry L s s = 2

@[simp]

theorem TauCeti.chainBEntry_succ_right (L s : ℕ) : chainBEntry L s (s + 1) = if s + 1 = L then -2 else -1

Stepping forwards along the chain crosses a double edge exactly at the short end.

@[simp]

theorem TauCeti.chainBEntry_succ_left (L s : ℕ) : chainBEntry L (s + 1) s = -1

Stepping backwards along the chain always crosses a single edge: the short root is the target of the double edge, not its source.

@[simp]

theorem TauCeti.chainBEntry_eq_zero {L s t : ℕ} (h1 : s ≠ t) (h2 : s + 1 ≠ t) (h3 : t + 1 ≠ s) : chainBEntry L s t = 0

Away from the diagonal and its two neighbours a chain has no entry.

theorem TauCeti.chainBEntry_eq_cartanMatrix_B {n : ℕ} (i j : Fin n) : chainBEntry (n - 1) ↑i ↑j = CartanMatrix.B n i j

A chain of type B is Mathlib's Cartan matrix of type B: on n positions the two entry rules agree.

theorem TauCeti.sum_range_chainBEntry_mul {R : Type u_1} [NonAssocRing R] {L m a : ℕ} (ha : a < m) (g : ℕ → R) : ∑ s ∈ Finset.range m, ↑(chainBEntry L a s) * g s = (2 * g a - if a = 0 then 0 else g (a - 1)) - if a + 1 = m then 0 else (if a + 1 = L then 2 else 1) * g (a + 1)

A row of a chain of type B, against an arbitrary weighting of its positions. The row a collects 2 g a, the weight of the position before it - absent at the head of the chain - and the weight of the position after it, doubled when that position is the short end and absent when the row is the last of the m positions.

def TauCeti.chainEntry (s t : ℕ) : ℤ

The Cartan-matrix entry of a chain between the positions s and t along it: 2 on the diagonal, -1 between consecutive positions, and 0 otherwise. A chain is simply laced, so this single function describes all of its edges.

Equations

• TauCeti.chainEntry s t = TauCeti.chainBEntry 0 s t

theorem TauCeti.chainEntry_def (s t : ℕ) : chainEntry s t = if s = t then 2 else if s = t + 1 then -1 else if t = s + 1 then -1 else 0

The entries of a chain, spelled out: this is how a file that has to case on all of them at once reaches the definition, whose body is not exposed.

@[simp]

theorem TauCeti.chainEntry_self (s : ℕ) : chainEntry s s = 2

@[simp]

theorem TauCeti.chainEntry_succ_left (s : ℕ) : chainEntry (s + 1) s = -1

@[simp]

theorem TauCeti.chainEntry_succ_right (s : ℕ) : chainEntry s (s + 1) = -1

@[simp]

theorem TauCeti.chainEntry_eq_zero {s t : ℕ} (h1 : s ≠ t) (h2 : s ≠ t + 1) (h3 : t ≠ s + 1) : chainEntry s t = 0

Away from the diagonal and its two neighbours a chain has no entry.

theorem TauCeti.chainEntry_succ_succ (s t : ℕ) : chainEntry (s + 1) (t + 1) = chainEntry s t

Shifting both positions of a chain by one leaves the entry unchanged: only the difference of the positions matters. This is not a simp lemma: it would rewrite the right-hand sides of the entry lemmas for TauCeti.starCartanMatrix, whose arm positions are shifted by one against the centre, out of the form those lemmas state.

theorem TauCeti.chainEntry_comm (s t : ℕ) : chainEntry s t = chainEntry t s

A chain is symmetric: the entry depends on the unordered pair of positions.

theorem TauCeti.chainEntry_eq_cartanMatrix_A {n : ℕ} (i j : Fin n) : chainEntry ↑i ↑j = CartanMatrix.A n i j

A chain is Mathlib's Cartan matrix of type A: on n positions the two entry rules agree.

theorem TauCeti.sum_range_chainEntry_mul {R : Type u_1} [NonAssocRing R] {n m : ℕ} (hm : m < n) (g : ℕ → R) : ∑ s ∈ Finset.range n, ↑(chainEntry m s) * g (s + 1) = (2 * g (m + 1) - if m = 0 then 0 else g m) - if m + 1 = n then 0 else g (m + 2)

The row of a chain, evaluated at a weight. Along n positions 1, …, n, carrying the weights g 1, …, g n, the entries at the position m collect 2 g (m + 1) - g m - g (m + 2), the term g m being absent at m = 0 and the term g (m + 2) at the far end. A weight that is linear in the position is therefore annihilated away from the two ends.

The offset by one in the argument of g leaves room for a further vertex at the position 0, to which the chain is attached in the diagrams assembled from it.

theorem TauCeti.sum_range_chainEntry_mul_affine {R : Type u_1} [NonAssocRing R] {n m : ℕ} (hm : m < n) (a b : R) : ∑ s ∈ Finset.range n, ↑(chainEntry m s) * (a * ↑s + b) = if m = 0 then if m + 1 = n then 2 * b else b - a else if m + 1 = n then a * ↑n + b else 0

A row of a chain evaluated at an affine weight. Interior rows vanish; the first row leaves b - a, the last row leaves a * n + b, and the unique row of a one-vertex chain leaves 2 * b.