Reindexing path-shaped diagrams with a double edge

The classification of the model matrices TauCeti.doubleEdgeCartanMatrix p q is already known: when both chains are nonempty, finite type leaves precisely the families B_n, C_n, and the exceptional type F_4. To apply that result to an arbitrary Cartan matrix, its diagram must first be reindexed onto the model.

This file performs that reindexing for the branchless case. A preconnected finite-type diagram in which every vertex has degree at most two is a path. After orienting the path so that a chosen double edge points from -1 to -2, cutting at that edge gives two nonempty chains. No other edge of the path is multiple: applying the affine-diagram exclusion TauCeti.IsFiniteType.apply_mul_apply_le_one_of_chain_of_two_le inductively along the path rules out a second one. Hence every other edge is simple, and the matrix itself -- not merely its underlying graph -- is TauCeti.doubleEdgeCartanMatrix p q after one simultaneous relabelling.

Main result

• TauCeti.IsFiniteType.exists_equiv_forall_eq_doubleEdgeCartanMatrix: a preconnected finite-type matrix of maximum degree two containing one oriented double edge reindexes to a nonempty TauCeti.doubleEdgeCartanMatrix p q.

This is the reindexing bridge in the double-edge branch of the classification of finite-type Cartan matrices under the degree-at-most-two hypothesis. Excluding branch vertices in a general connected diagram containing a double edge is a separate result. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, section 11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, section 4.

The double-edge model read along its path

Reindexing a path-shaped diagram

A path carries at most one multiple edge

theorem TauCeti.IsFiniteType.exists_equiv_forall_eq_doubleEdgeCartanMatrix {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] [DecidableEq B] (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) (hdeg : ∀ (i : B), (diagramGraph A).degree i ≤ 2) {u v : B} (hvu : A v u = -2) : ∃ (p : ℕ) (q : ℕ), 0 < p ∧ 0 < q ∧ ∃ (e : B ≃ Fin p ⊕ Fin q), ∀ (i j : B), A i j = doubleEdgeCartanMatrix p q (e i) (e j)

A path-shaped finite-type matrix containing an oriented double edge is a double-edge model. Suppose the diagram is preconnected, every vertex has degree at most two, and the edge u -- v carries A v u = -2. Then there are nonempty chains of lengths p and q and a simultaneous relabelling under which A is TauCeti.doubleEdgeCartanMatrix p q.

Nothing is assumed about the other edges: the path argument above proves that the chosen edge is the only multiple edge, and the finite-type sign conditions then determine every remaining nonzero entry.