The diagram of a finite-type Cartan matrix is a forest

The elimination tools of TauCeti.LinearAlgebra.RootSystem.FiniteType.Basic are stated entrywise: they say that certain patterns of nonzero entries cannot occur together. The classification of finite-type Cartan matrices reads them as statements about a graph, the diagram of the matrix, whose vertices are the indices and whose edges are the nonzero off-diagonal pairs. This file introduces that graph and records the two global shape theorems the classification runs on: the diagram of a finite-type matrix is acyclic, and every vertex of it has degree at most 3. A connected finite-type diagram is therefore a tree, with exactly one fewer edge than it has vertices, and the Dynkin diagram of an irreducible root system is one such tree.

Acyclicity is the graph form of TauCeti.IsFiniteType.exists_apply_succ_eq_zero, whose statement is about a cyclic list of indices; the list is supplied by Mathlib's characterization of acyclicity as containing no copy of a cycle graph, SimpleGraph.isAcyclic_iff_free_cycleGraph. Connectedness in the root-system case is irreducibility, which Mathlib packages as RootPairing.Base.induction_on_cartanMatrix.

Main definitions

• TauCeti.diagramGraph: the diagram of an integer matrix, a SimpleGraph on its index type, joining two distinct indices when the entries of the transposed pair are both nonzero.

Main results

• TauCeti.diagramGraph_submatrix: the diagram of a principal submatrix is the pullback of the diagram along the reindexing.
• TauCeti.DynkinType.diagramGraph_cartanMatrix_A: the type Aₙ diagram is the path graph on n nodes.
• TauCeti.IsFiniteType.isAcyclic_diagramGraph: the diagram of a finite-type matrix is a forest. The affine diagrams Ãₙ for n ≥ 2, the ones whose diagrams are cycles, are excluded here in one theorem.
• TauCeti.IsFiniteType.exists_chain_of_reachable: two vertices in the same component are joined by a chain of distinct indices whose consecutive matrix entries are nonzero and whose nonconsecutive entries vanish. This is the bridge from graph paths to the principal-submatrix arguments used in the classification.
• TauCeti.IsFiniteType.degree_le_three: the degree bound, in graph form.
• TauCeti.IsFiniteType.isTree_diagramGraph and TauCeti.IsFiniteType.card_edgeFinset_add_one_eq_card: a connected finite-type diagram is a tree, and so has one fewer edge than it has vertices.
• TauCeti.isTree_diagramGraph_cartanMatrix and TauCeti.card_edgeFinset_add_one_eq_card_support: the Dynkin diagram of an irreducible reduced crystallographic finite root system is a tree, whose edges number one fewer than its simple roots. Connectedness is TauCeti.preconnected_diagramGraph_cartanMatrix.

References

This file supplies the "no cycles" and "n - 1 edges" steps 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, where the shape of an admissible diagram is deduced from exactly these two facts, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4.

def TauCeti.diagramGraph {B : Type u_1} (A : Matrix B B ℤ) : SimpleGraph B

The diagram of an integer matrix: the graph on the index type joining two distinct indices when both entries of the transposed pair are nonzero.

For a generalized Cartan matrix, and so for a matrix of finite type, one of the two entries is nonzero exactly when the other is (TauCeti.IsFiniteType.diagramGraph_adj_iff), and the definition is the expected one. Asking for both is what makes the relation symmetric for an arbitrary matrix, where it is the diagram of the symmetrized vanishing pattern; the symmetrization that SimpleGraph.fromRel performs is then a duplication, and TauCeti.diagramGraph_adj reads the adjacency back off.

Equations

• TauCeti.diagramGraph A = SimpleGraph.fromRel fun (i j : B) => A i j ≠ 0 ∧ A j i ≠ 0

@[simp]

theorem TauCeti.diagramGraph_adj {B : Type u_1} {A : Matrix B B ℤ} {i j : B} : (diagramGraph A).Adj i j ↔ i ≠ j ∧ A i j ≠ 0 ∧ A j i ≠ 0

@[instance_reducible]

instance TauCeti.instDecidableRelAdjDiagramGraphOfDecidableEq {B : Type u_1} [DecidableEq B] (A : Matrix B B ℤ) : DecidableRel (diagramGraph A).Adj

Equations

• TauCeti.instDecidableRelAdjDiagramGraphOfDecidableEq A x✝¹ x✝ = decidable_of_iff (x✝¹ ≠ x✝ ∧ A x✝¹ x✝ ≠ 0 ∧ A x✝ x✝¹ ≠ 0) ⋯

theorem TauCeti.diagramGraph_submatrix {B : Type u_1} {C : Type u_2} {f : C → B} (hf : Function.Injective f) (A : Matrix B B ℤ) : diagramGraph (A.submatrix f f) = SimpleGraph.comap f (diagramGraph A)

The diagram of a principal submatrix is the pullback of the diagram. Restricting a matrix to an injectively indexed family of indices deletes from its diagram exactly the vertices outside that family, keeping every edge between two of the remaining ones.

@[simp]

theorem TauCeti.DynkinType.diagramGraph_cartanMatrix_A (n : ℕ) : diagramGraph (CartanMatrix.A n) = SimpleGraph.pathGraph n

The diagram of type Aₙ is the path graph: in Bourbaki's numbering, the nodes i and j are joined exactly when they are consecutive.

theorem TauCeti.diagramGraph_A_adj (n : ℕ) (i j : Fin n) : (diagramGraph (DynkinType.A n).cartanMatrix).Adj i j ↔ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i

Two nodes of the Aₙ diagram are joined exactly when they are consecutive.

theorem TauCeti.IsFiniteType.diagramGraph_adj_iff {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {i j : B} : (diagramGraph A).Adj i j ↔ i ≠ j ∧ A i j ≠ 0

Adjacency in the diagram of a finite-type matrix is a single nonvanishing condition, the vanishing pattern of such a matrix being symmetric.

theorem TauCeti.IsFiniteType.isAcyclic_diagramGraph {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) : (diagramGraph A).IsAcyclic

The diagram of a finite-type matrix is a forest. No walk of the diagram that returns to its start is a cycle.

A cycle in a graph is a copy of a cycle graph of length at least three (SimpleGraph.isAcyclic_iff_free_cycleGraph), so its vertices are a list of at least three distinct indices each joined to its cyclic successor, which is what TauCeti.IsFiniteType.exists_apply_succ_eq_zero forbids.

theorem TauCeti.IsFiniteType.exists_chain_of_reachable {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {u v : B} (huv : (diagramGraph A).Reachable u v) : ∃ (n : ℕ) (w : ℕ → B), w 0 = u ∧ w n = v ∧ Set.InjOn w {i : ℕ | i ≤ n} ∧ (∀ i < n, A (w i) (w (i + 1)) ≠ 0) ∧ ∀ (i j : ℕ), i + 1 < j → j ≤ n → A (w i) (w j) = 0

A reachable pair in a finite-type diagram is joined by an induced matrix chain. More precisely, there are vertices w 0, ..., w n with the prescribed endpoints, no repetitions, nonzero entries between consecutive vertices, and zero entries between vertices separated by at least one intermediate vertex.

The no-chord conclusion is the part not supplied merely by choosing a graph path. It follows from the diagram being acyclic, and is what lets a classification argument identify the corresponding principal submatrix with a chain-shaped model rather than only a matrix containing the chain's edges. Nothing is asserted about vertices outside the chain.

theorem TauCeti.IsFiniteType.degree_le_three {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] [DecidableEq B] (h : IsFiniteType A) (i : B) : (diagramGraph A).degree i ≤ 3

The degree bound in graph form: no index of a finite-type matrix has four neighbours in the diagram, so a finite-type diagram branches into at most three arms.

theorem TauCeti.IsFiniteType.isTree_diagramGraph {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) : (diagramGraph A).IsTree

A connected finite-type diagram is a tree. For the Cartan matrix of a base this is the irreducible case, the one the classification enumerates.

theorem TauCeti.IsFiniteType.card_edgeFinset_add_one_eq_card {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] [DecidableEq B] (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) : (diagramGraph A).edgeFinset.card + 1 = Fintype.card B

A connected finite-type diagram has one edge fewer than it has vertices. This is the counting form of acyclicity, and the constraint that the enumeration of admissible diagrams is run against.

theorem TauCeti.preconnected_diagramGraph_cartanMatrix {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] (b : P.Base) : (diagramGraph b.cartanMatrix).Preconnected

The Dynkin diagram of an irreducible root system is connected. Irreducibility of a root pairing says that the roots do not split into two mutually orthogonal families, and Mathlib records it as the induction principle RootPairing.Base.induction_on_cartanMatrix: a property of the simple roots that propagates along nonzero Cartan entries holds everywhere once it holds somewhere. Being reachable from a fixed simple root is such a property.

theorem TauCeti.connected_diagramGraph_cartanMatrix {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [Nonempty ι] [P.IsReduced] [P.IsIrreducible] (b : P.Base) : (diagramGraph b.cartanMatrix).Connected

The Dynkin diagram of an irreducible root system is connected, as a Connected graph: a root system with at least one root has at least one simple root.

theorem TauCeti.isTree_diagramGraph_cartanMatrix {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [Nonempty ι] [P.IsRootSystem] [P.IsReduced] [P.IsIrreducible] (b : P.Base) : (diagramGraph b.cartanMatrix).IsTree

The Dynkin diagram of an irreducible root system is a tree. Both halves are theorems about the Cartan matrix: acyclicity because it is of finite type, connectedness because the root system is irreducible.

theorem TauCeti.card_edgeFinset_add_one_eq_card_support {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [Nonempty ι] [P.IsRootSystem] [P.IsReduced] [P.IsIrreducible] (b : P.Base) [DecidableEq ↥b.support] : (diagramGraph b.cartanMatrix).edgeFinset.card + 1 = b.support.card

The Dynkin diagram of an irreducible root system has one edge fewer than it has simple roots. With the degree bound of TauCeti.IsFiniteType.degree_le_three, this is the shape constraint that the enumeration of the admissible diagrams is run against.