The Cartan matrix of a graph carrying a positive additive function

For a finite simple graph G with adjacency matrix A, the matrix 2I - A is the generalized Cartan matrix of G read as a simply-laced diagram. This file proves that 2I - A is positive semidefinite as soon as G carries a positive additive function, a vector δ with

∑_{j ∼ i} δ j = 2 * δ i

at every node, and that for a connected G the radical of the associated form is then exactly the line spanned by δ.

The proof is a weighted version of the Laplacian identity SimpleGraph.lapMatrix_toLinearMap₂'. Writing a vector as x = δ * y, the additive condition turns the quadratic form into a sum of squares over the oriented edges,

2 * (δy)ᵀ (2I - A) (δy) = ∑_i ∑_{j ∼ i} δ i * δ j * (y i - y j)²

(SimpleGraph.two_mul_dotProduct_graphCartanMatrix_mulVec). Nonnegativity is immediate; the form vanishes exactly when y is constant along edges, hence — on a connected graph — constant. Note that 2I - A is not the Laplacian D - A unless G is 2-regular, so Mathlib's Laplacian results do not apply directly: the additive function replaces 2-regularity, and δ i * δ j is the edge weight it induces.

Kac calls such a δ an additive function, and a connected simple graph admits a positive one exactly when it is a graphical affine diagram (so excluding the multiplicity-two diagram A₁). That classification is not proved here; the results below take δ as given.

Main definitions

• SimpleGraph.graphCartanMatrix: the matrix 2I - A of a simple graph.

Main results

• SimpleGraph.graphCartanMatrix_mulVec_eq_zero: an additive function is a null vector.
• SimpleGraph.two_mul_dotProduct_graphCartanMatrix_mulVec: the sum-of-squares identity.
• SimpleGraph.dotProduct_graphCartanMatrix_mulVec_eq_zero_iff_forall_adj and SimpleGraph.graphCartanMatrix_mulVec_eq_zero_iff_forall_adj: the vanishing criterion, in quadratic-form and in null-vector shape.
• SimpleGraph.posSemidef_graphCartanMatrix: 2I - A is positive semidefinite.
• SimpleGraph.ker_mulVecLin_graphCartanMatrix: on a preconnected graph the null space of 2I - A is the span of the additive function.

References

V. Kac, Infinite dimensional Lie algebras, 3rd ed., Chapter 4, where positive additive functions single out the affine diagrams.

Adapted from Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean (Adrian Wüthrich, Apache-2.0): the development of this file follows it declaration for declaration, with the additive-function weight δ i * δ j replacing 2-regularity. In particular SimpleGraph.graphCartanMatrix, SimpleGraph.graphCartanMatrix_mulVec_apply, SimpleGraph.isSymm_graphCartanMatrix and SimpleGraph.graphCartanMatrix_mulVec_eq_zero mirror SimpleGraph.lapMatrix, SimpleGraph.lapMatrix_mulVec_apply, SimpleGraph.isSymm_lapMatrix and SimpleGraph.lapMatrix_mulVec_const_eq_zero, while the proofs of SimpleGraph.posSemidef_graphCartanMatrix, SimpleGraph.graphCartanMatrix_mulVec_eq_zero_iff_forall_adj and the walk induction in SimpleGraph.ker_mulVecLin_graphCartanMatrix are adapted from SimpleGraph.posSemidef_lapMatrix, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj and the walk induction inside SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable.

def SimpleGraph.graphCartanMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Ring R] : Matrix V V R

The generalized Cartan matrix 2I - A of a simple graph, read as a simply-laced diagram: 2 on the diagonal, -1 at an edge and 0 elsewhere. Unlike the Laplacian SimpleGraph.lapMatrix, whose diagonal records the degrees, this matrix has a constant diagonal.

Equations

• G.graphCartanMatrix R = 2 • 1 - SimpleGraph.adjMatrix R G

theorem SimpleGraph.graphCartanMatrix_eq_two_smul_one_sub_adjMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Ring R] : G.graphCartanMatrix R = 2 • 1 - adjMatrix R G

2I - A spelled out as a matrix, for a consumer outside this file: the body of SimpleGraph.graphCartanMatrix is not exposed.

@[simp]

theorem SimpleGraph.graphCartanMatrix_apply {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Ring R] (i j : V) : G.graphCartanMatrix R i j = if i = j then 2 else if G.Adj i j then -1 else 0

The entries of 2I - A: 2 on the diagonal, -1 at an edge and 0 elsewhere.

@[simp]

theorem SimpleGraph.graphCartanMatrix_map {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] (f : R →+* S) : (G.graphCartanMatrix R).map ⇑f = G.graphCartanMatrix S

2I - A is compatible with a change of coefficient ring.

theorem SimpleGraph.isSymm_graphCartanMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Ring R] : (G.graphCartanMatrix R).IsSymm

2I - A is symmetric.

theorem SimpleGraph.graphCartanMatrix_mulVec_apply {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Ring R] (x : V → R) (i : V) : (G.graphCartanMatrix R).mulVec x i = 2 * x i - ∑ j ∈ G.neighborFinset i, x j

Multiplying a vector by 2I - A doubles it and subtracts the sum over its neighbours.

theorem SimpleGraph.graphCartanMatrix_mulVec_eq_zero {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Ring R] {δ : V → R} (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) : (G.graphCartanMatrix R).mulVec δ = 0

An additive function is a null vector of 2I - A. Positivity is not needed: the balance condition alone says that 2 δ i is the sum of the neighbouring values.

theorem SimpleGraph.two_mul_dotProduct_graphCartanMatrix_mulVec {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [CommRing R] {δ : V → R} (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) (y : V → R) : 2 * (δ * y) ⬝ᵥ (G.graphCartanMatrix R).mulVec (δ * y) = ∑ i : V, ∑ j ∈ G.neighborFinset i, δ i * δ j * (y i - y j) ^ 2

The sum-of-squares identity for a graph with an additive function. After the substitution x = δ * y, twice the quadratic form of 2I - A at x is the sum, over the oriented edges, of δ i * δ j * (y i - y j) ². This is the weighted analogue of SimpleGraph.lapMatrix_toLinearMap₂', with the edge weight δ i * δ j in place of 1, and it is where the additive condition on δ enters.

theorem SimpleGraph.dotProduct_graphCartanMatrix_mulVec_nonneg {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {δ : V → R} (hpos : ∀ (i : V), 0 < δ i) (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) (x : V → R) : 0 ≤ x ⬝ᵥ (G.graphCartanMatrix R).mulVec x

The quadratic form of 2I - A is nonnegative on a graph with a positive additive function.

theorem SimpleGraph.dotProduct_graphCartanMatrix_mulVec_eq_zero_iff_forall_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {δ : V → R} (hpos : ∀ (i : V), 0 < δ i) (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) (x : V → R) : x ⬝ᵥ (G.graphCartanMatrix R).mulVec x = 0 ↔ ∀ (i j : V), G.Adj i j → x i * δ j = x j * δ i

The quadratic form of 2I - A vanishes exactly on the vectors proportional to δ along every edge. The stated condition is x i / δ i = x j / δ j cleared of denominators.

theorem SimpleGraph.posSemidef_graphCartanMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {δ : V → R} [StarRing R] [TrivialStar R] (hpos : ∀ (i : V), 0 < δ i) (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) : (G.graphCartanMatrix R).PosSemidef

2I - A is positive semidefinite on a graph with a positive additive function.

theorem SimpleGraph.graphCartanMatrix_mulVec_eq_zero_iff_forall_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {δ : V → R} (hpos : ∀ (i : V), 0 < δ i) (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) (x : V → R) : (G.graphCartanMatrix R).mulVec x = 0 ↔ ∀ (i j : V), G.Adj i j → x i * δ j = x j * δ i

The null vectors of 2I - A, in edge-local form.

theorem SimpleGraph.ker_mulVecLin_graphCartanMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_2} [Fintype V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {δ : V → R} (hG : G.Preconnected) (hpos : ∀ (i : V), 0 < δ i) (hδ : ∀ (i : V), ∑ j ∈ G.neighborFinset i, δ j = 2 * δ i) : (G.graphCartanMatrix R).mulVecLin.ker = R ∙ δ

On a preconnected graph the null space of 2I - A is the line spanned by the additive function. This also covers the empty graph, where both subspaces are zero. Since 2I - A is positive semidefinite, this is the radical of its bilinear form.