Simple graphs of finite type

A finite simple graph G with adjacency matrix A is read as a simply-laced diagram through its generalized Cartan matrix 2I - A (SimpleGraph.graphCartanMatrix). This file connects that matrix with the finite-type Cartan matrices of TauCeti.IsFiniteType and their classification: the diagram of 2I - A is G itself, a positive definite 2I - A over any linear ordered field is of finite type, and a connected graph whose 2I - A is of finite type is isomorphic to the diagram of the standard Cartan matrix of a valid simply-laced Dynkin type. In other words, a connected simple graph has a positive definite form 2I - A exactly when it is a Dynkin diagram of type A, D or E.

Main results

• SimpleGraph.diagramGraph_graphCartanMatrix: the diagram of 2I - A is G.
• SimpleGraph.isFiniteType_graphCartanMatrix_of_posDef: if 2I - A is positive definite over a linear ordered field, then it is of finite type.
• SimpleGraph.exists_dynkinType_iso_of_isFiniteType_graphCartanMatrix: a connected graph whose 2I - A is of finite type is isomorphic to the diagram of a valid simply-laced Dynkin type.
• SimpleGraph.graphCartanMatrix_diagramGraph_cartanMatrix: the standard Cartan matrix of a Dynkin type whose Cartan matrix is simply laced is 2I - A of its diagram.
• SimpleGraph.posDef_graphCartanMatrix_iff: a connected graph has a positive definite 2I - A exactly when it is isomorphic to the diagram of a valid simply-laced Dynkin type.
• TauCeti.DynkinType.exists_isSimplyLaced_diagramGraph_iso and SimpleGraph.exists_valid_isSimplyLaced_dynkinType_iso_iff: every standard Dynkin diagram is isomorphic as a simple graph to the diagram of a simply-laced Dynkin type.
• TauCeti.DynkinType.isAcyclic_diagramGraph_cartanMatrix and TauCeti.DynkinType.isBipartite_diagramGraph_cartanMatrix: every standard Dynkin diagram is acyclic and bipartite.
• SimpleGraph.exists_pos_two_mul_le_sum_of_not_exists_dynkinType_iso: a connected graph which is not a Dynkin diagram carries a positive weight δ with 2 δ i ≤ ∑_{j ∼ i} δ j at every vertex; such a graph has no isolated vertex (SimpleGraph.exists_adj_of_pos_two_mul_le_sum, in Combinatorics/SimpleGraph/AdditiveFunction.lean).

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.
• V. G. Kac, Infinite dimensional Lie algebras, 3rd ed., Chapter 4.

@[simp]

theorem SimpleGraph.diagramGraph_graphCartanMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : TauCeti.diagramGraph (G.graphCartanMatrix ℤ) = G

The diagram of the generalized Cartan matrix 2I - A of a simple graph is the graph itself.

theorem SimpleGraph.isFiniteType_graphCartanMatrix_of_posDef {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Finite V] {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [StarRing R] (h : (G.graphCartanMatrix R).PosDef) : TauCeti.IsFiniteType (G.graphCartanMatrix ℤ)

A positive definite graph Cartan matrix is of finite type. If 2I - A is positive definite over some linear ordered field, then the integer matrix 2I - A is of finite type.

theorem SimpleGraph.exists_dynkinType_iso_of_isFiniteType_graphCartanMatrix {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (hG : G.Connected) (h : TauCeti.IsFiniteType (G.graphCartanMatrix ℤ)) : ∃ (t : TauCeti.DynkinType), t.Valid ∧ t.IsSimplyLaced ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)

A connected graph of finite type is a simply-laced Dynkin diagram. If the generalized Cartan matrix 2I - A of a connected simple graph G is of finite type, then G is isomorphic to the diagram of the standard Cartan matrix of a valid Dynkin type, which is of type A, D or E: the standard matrix is a relabelling of 2I - A, whose off-diagonal entries are 0 or -1.

@[simp]

theorem SimpleGraph.graphCartanMatrix_diagramGraph_cartanMatrix {t : TauCeti.DynkinType} (ht : t.cartanMatrix.IsSimplyLaced) : (TauCeti.diagramGraph t.cartanMatrix).graphCartanMatrix ℤ = t.cartanMatrix

The diagram of a simply-laced standard Cartan matrix recovers that matrix: for a Dynkin type whose Cartan matrix is simply laced, the matrix is 2I - A of its diagram.

theorem TauCeti.DynkinType.exists_isSimplyLaced_diagramGraph_iso (t : DynkinType) : ∃ (s : DynkinType), s.IsSimplyLaced ∧ (t.Valid → s.Valid) ∧ Nonempty (diagramGraph t.cartanMatrix ≃g diagramGraph s.cartanMatrix)

Every standard Dynkin diagram is isomorphic to the diagram of a simply-laced Dynkin type of the same rank (preserving validity), since the underlying simple graphs of Bₙ, Cₙ, F₄, and G₂ are path graphs.

theorem SimpleGraph.posDef_graphCartanMatrix_of_iso {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {t : TauCeti.DynkinType} (φ : G ≃g TauCeti.diagramGraph t.cartanMatrix) : (G.graphCartanMatrix ℚ).PosDef

A graph isomorphic to the diagram of a standard Cartan matrix has a positive definite 2I - A. The underlying graph of every standard Dynkin diagram is isomorphic to that of a simply-laced one (TauCeti.DynkinType.exists_isSimplyLaced_diagramGraph_iso), whose matrix 2I - A is the standard Cartan matrix (SimpleGraph.graphCartanMatrix_diagramGraph_cartanMatrix), which is positive definite; an isomorphism of graphs relabels 2I - A.

theorem SimpleGraph.posDef_graphCartanMatrix_iff {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Finite V] (hG : G.Connected) : (G.graphCartanMatrix ℚ).PosDef ↔ ∃ (t : TauCeti.DynkinType), t.Valid ∧ t.IsSimplyLaced ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)

A connected graph has a positive definite 2I - A exactly when it is a simply-laced Dynkin diagram, that is, isomorphic to the diagram of a valid Dynkin type of type A, D or E.

theorem TauCeti.DynkinType.isAcyclic_diagramGraph_cartanMatrix (t : DynkinType) : (diagramGraph t.cartanMatrix).IsAcyclic

Every standard Dynkin diagram is acyclic.

theorem TauCeti.DynkinType.isBipartite_diagramGraph_cartanMatrix (t : DynkinType) : (diagramGraph t.cartanMatrix).IsBipartite

Every standard Dynkin diagram is bipartite.

theorem SimpleGraph.exists_valid_isSimplyLaced_dynkinType_iso_iff {V : Type u_1} (G : SimpleGraph V) : (∃ (t : TauCeti.DynkinType), t.Valid ∧ t.IsSimplyLaced ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)) ↔ ∃ (t : TauCeti.DynkinType), t.Valid ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)

A simple graph is isomorphic to the diagram of a valid simply-laced Dynkin type if and only if it is isomorphic to the diagram of a valid Dynkin type.

Superadditive weights on graphs of infinite type

theorem SimpleGraph.exists_nonneg_two_mul_le_sum_of_not_posDef {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] (h : ¬(G.graphCartanMatrix ℝ).PosDef) : ∃ (δ : V → ℝ), 0 ≤ δ ∧ δ ≠ 0 ∧ ∀ (i : V), 2 * δ i ≤ ∑ j ∈ G.neighborFinset i, δ j

A graph whose 2I - A is not positive definite carries a superadditive weight: a nonzero nonnegative real weight δ with 2 δ i ≤ ∑_{j ∼ i} δ j at every vertex.

theorem SimpleGraph.exists_pos_two_mul_le_sum_of_not_exists_dynkinType_iso {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] (hG : G.Connected) (hD : ¬∃ (t : TauCeti.DynkinType), t.Valid ∧ Nonempty (G ≃g TauCeti.diagramGraph t.cartanMatrix)) : ∃ (δ : V → ℝ), (∀ (i : V), 0 < δ i) ∧ ∀ (i : V), 2 * δ i ≤ ∑ j ∈ G.neighborFinset i, δ j

A connected non-Dynkin graph carries a positive superadditive weight. If a connected finite simple graph G is not isomorphic to the diagram of any valid Dynkin type, then some real weight δ, positive at every vertex, satisfies 2 δ i ≤ ∑_{j ∼ i} δ j at every vertex.