Kirchhoff's matrix-tree theorem

DefinitionInteger Laplacian of a graph#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\), the integer Laplacian of \(G\) is the \(V \times V\) integer matrix \(L\) with \(L_{uu} = \deg u\) for every vertex \(u\), \(L_{uv} = -1\) when \(u \ne v\) are adjacent, and \(L_{uv} = 0\) when \(u \ne v\) are not adjacent.

def laplacianInt {V : Type*} [Fintype V] [DecidableEq V] (G : _root_.SimpleGraph V)
    [DecidableRel G.Adj] : Matrix V V ℤ :=
  Matrix.of fun u v => if u = v then (G.degree u : ℤ) else if G.Adj u v then -1 else 0

Used by 4

Used byMatrix-tree theorem for a chosen root · The integer Laplacian is degree minus adjacency · Reduced Laplacian · The reduced Laplacian is a principal submatrix

DefinitionReduced Laplacian#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\) and a vertex \(r \in V\), the reduced Laplacian of \(G\) at \(r\) is the integer Laplacian of \(G\) with the row and the column of \(r\) deleted, a matrix indexed by the vertices of \(G\) other than \(r\).

def reducedLaplacian {V : Type*} [Fintype V] [DecidableEq V] (G : _root_.SimpleGraph V)
    [DecidableRel G.Adj] (root : V) :
    Matrix { v : V // v ≠ root } { v : V // v ≠ root } ℤ :=
  Matrix.of fun ⟨u, _⟩ ⟨v, _⟩ => laplacianInt G u v

Uses 1 · Used by 4

Statement usesInteger Laplacian of a graph

Used byKirchhoff's matrix-tree theorem · Matrix-tree theorem for principal minors of the Laplacian · Matrix-tree theorem for a chosen root · The reduced Laplacian is a principal submatrix

DefinitionSpanning tree#✓fully proved

A subgraph \(T\) of a simple graph \(G\) is a spanning tree of \(G\) if it contains every vertex of \(G\) and, regarded as a graph on its own vertex set, it is a tree (connected and acyclic).

def IsSpanningTree {V : Type*} {G : _root_.SimpleGraph V} (T : G.Subgraph) : Prop :=
  T.IsSpanning ∧ T.coe.IsTree

Used by 5

Used byCayley's formula · Matrix-tree theorem for a chosen root · Number of spanning trees · Spanning trees as trees on the whole vertex set · Spanning trees as trees contained in the graph

DefinitionNumber of spanning trees#✓fully proved

For a simple graph \(G\) on a finite vertex set, the number of spanning trees of \(G\) is the number of subgraphs of \(G\) that are spanning trees, that is, subgraphs that contain every vertex of \(G\) and are trees.

noncomputable def numSpanningTrees {V : Type*} (G : _root_.SimpleGraph V) [Fintype V]
    [DecidableRel G.Adj] : ℕ :=
  Nat.card { T : G.Subgraph // IsSpanningTree T }

Uses 1 · Used by 5

Statement usesSpanning tree

Used byCayley's formula · Kirchhoff's matrix-tree theorem · Matrix-tree theorem for principal minors of the Laplacian · Matrix-tree theorem for a chosen root · Spanning trees as trees on the whole vertex set

TheoremThe integer Laplacian is degree minus adjacency#✓fully proved

For a simple graph \(G\) on a finite vertex set, the integer Laplacian of \(G\) equals \(D - A\), where \(D\) is the diagonal matrix of vertex degrees and \(A\) is the adjacency matrix of \(G\), both with integer entries.

theorem laplacianInt_eq_lapMatrix {V : Type*} [Fintype V] [DecidableEq V]
    (G : _root_.SimpleGraph V) [DecidableRel G.Adj] :
    laplacianInt G = G.lapMatrix ℤ

Uses 1 · Used by 1

Statement usesInteger Laplacian of a graph

Used byThe reduced Laplacian is a principal submatrix

TheoremThe reduced Laplacian is a principal submatrix#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(L = D - A\) be its Laplacian matrix over \(\mathbb{Z}\), where \(D\) is the diagonal matrix of vertex degrees and \(A\) is the adjacency matrix of \(G\). For every vertex \(r \in V\), the reduced Laplacian of \(G\) at \(r\) equals the submatrix of \(L\) obtained by deleting the row and the column of \(r\).

theorem reducedLaplacian_eq_lapMatrix_submatrix {V : Type*} [Fintype V] [DecidableEq V]
    (G : _root_.SimpleGraph V) [DecidableRel G.Adj] (root : V) :
    reducedLaplacian G root =
      (G.lapMatrix ℤ).submatrix Subtype.val Subtype.val

Uses 3 · Used by 1

Statement usesReduced Laplacian

Proof usesInteger Laplacian of a graph · The integer Laplacian is degree minus adjacency

Used byMatrix-tree theorem for principal minors of the Laplacian

DefinitionSpanning trees as trees contained in the graph#✓fully proved

For a simple graph \(G\) on a vertex set \(V\), there is an equivalence between the spanning trees of \(G\) (subgraphs of \(G\) that contain every vertex and are trees) and the simple graphs \(H\) on \(V\) that are trees with \(H \le G\), that is, every edge of \(H\) is an edge of \(G\). It sends a spanning tree to the graph on \(V\) with the same edges.

MathlibExt.Combinatorics.SimpleGraph.MatrixTreeWanted.spanningTreeSubgraphEquiv · 37 lines

def spanningTreeSubgraphEquiv {V : Type*} (G : SimpleGraph V) :
    {T : G.Subgraph // IsSpanningTree T} ≃ {H : SimpleGraph V // H ≤ G ∧ H.IsTree} := by
  classical
  refine
    { toFun := fun T => ⟨T.1.spanningCoe, T.1.spanningCoe_le, ?_⟩
      invFun := fun H => ⟨SimpleGraph.toSubgraph H.1 H.2.1,
        SimpleGraph.toSubgraph.isSpanning H.1 H.2.1, ?_⟩
      left_inv := ?_
      right_inv := ?_ }
  · exact (SimpleGraph.Iso.isTree_iff (T.1.spanningCoeEquivCoeOfSpanning T.2.1)).mpr T.2.2
  · obtain ⟨H, hle, htreeH⟩ := H
    have hspan_eq : (SimpleGraph.toSubgraph H hle).spanningCoe = H := by
      apply SimpleGraph.ext
      funext v w
      rw [SimpleGraph.Subgraph.spanningCoe_adj, SimpleGraph.toSubgraph_adj]
    have h1 : (SimpleGraph.toSubgraph H hle).spanningCoe.IsTree := hspan_eq.symm ▸ htreeH
    exact (SimpleGraph.Iso.isTree_iff
      (SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning _
        (SimpleGraph.toSubgraph.isSpanning H hle))).mp h1
  · intro T
    obtain ⟨T, hTspan, hTtree⟩ := T
    apply Subtype.ext
    change SimpleGraph.toSubgraph T.spanningCoe T.spanningCoe_le = T
    apply SimpleGraph.Subgraph.ext
    · have hv1 : (SimpleGraph.toSubgraph T.spanningCoe T.spanningCoe_le).verts = Set.univ :=
        SimpleGraph.Subgraph.isSpanning_iff.mp (SimpleGraph.toSubgraph.isSpanning _ _)
      have hv2 : T.verts = Set.univ := SimpleGraph.Subgraph.isSpanning_iff.mp hTspan
      rw [hv1, hv2]
    · funext v w
      rw [SimpleGraph.toSubgraph_adj, SimpleGraph.Subgraph.spanningCoe_adj]
  · intro H
    obtain ⟨H, hle, htreeH⟩ := H
    apply Subtype.ext
    change (SimpleGraph.toSubgraph H hle).spanningCoe = H
    apply SimpleGraph.ext
    funext v w
    rw [SimpleGraph.Subgraph.spanningCoe_adj, SimpleGraph.toSubgraph_adj]

Uses 1 · Used by 2

Statement usesSpanning tree

Used byMatrix-tree theorem for a chosen root · Spanning trees as trees on the whole vertex set

TheoremSpanning trees as trees on the whole vertex set#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\), the number of spanning trees of \(G\) equals the number of simple graphs \(H\) on \(V\) such that every edge of \(H\) is an edge of \(G\) and \(H\) is a tree.

theorem numSpanningTrees_eq_card_trees {V : Type*} [Fintype V]
    (G : SimpleGraph V) [DecidableRel G.Adj] :
    numSpanningTrees G = Nat.card {H : SimpleGraph V // H ≤ G ∧ H.IsTree}

Uses 3

Statement usesNumber of spanning trees

Proof usesSpanning tree · Spanning trees as trees contained in the graph

TheoremMatrix-tree theorem for a chosen root#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(r \in V\). Then the determinant of the reduced Laplacian of \(G\) at \(r\), that is, the integer Laplacian of \(G\) with the row and the column of \(r\) deleted, equals the number of spanning trees of \(G\).

No separate nonemptiness hypothesis on \(V\) is needed, since \(r\) is a vertex.

theorem kirchhoff_matrix_tree_of_root :
    ∀ {V : Type*} (G : _root_.SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
      (root : V),
      (reducedLaplacian G root).det = (numSpanningTrees G : ℤ)

Uses 5 · Used by 2

Statement usesNumber of spanning trees · Reduced Laplacian

Proof usesSpanning tree · Integer Laplacian of a graph · Spanning trees as trees contained in the graph

Used byKirchhoff's matrix-tree theorem · Matrix-tree theorem for principal minors of the Laplacian

TheoremMatrix-tree theorem for principal minors of the Laplacian#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), let \(L = D - A\) be its Laplacian matrix over \(\mathbb{Z}\), where \(D\) is the diagonal matrix of vertex degrees and \(A\) is the adjacency matrix of \(G\), and let \(r \in V\). Then the determinant of the submatrix of \(L\) obtained by deleting the row and the column of \(r\) equals the number of spanning trees of \(G\).

theorem kirchhoff_matrix_tree_lapMatrix :
    ∀ {V : Type*} (G : _root_.SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
      (root : V),
      ((G.lapMatrix ℤ).submatrix (Subtype.val : { v : V // v ≠ root } → V)
        (Subtype.val : { v : V // v ≠ root } → V)).det
        = (numSpanningTrees G : ℤ)

Uses 4

Statement usesNumber of spanning trees

Proof usesMatrix-tree theorem for a chosen root · Reduced Laplacian · The reduced Laplacian is a principal submatrix

TheoremKirchhoff's matrix-tree theorem#✓fully proved

Let \(G\) be a simple graph on a finite nonempty vertex set \(V\) and let \(r \in V\). Then the determinant of the reduced Laplacian of \(G\) at \(r\), that is, the integer Laplacian of \(G\) with the row and the column of \(r\) deleted, equals the number of spanning trees of \(G\).

In particular, this determinant is \(0\) when \(G\) is disconnected.

theorem kirchhoff_matrix_tree :
    ∀ {V : Type*} (G : _root_.SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
      [Nonempty V] (root : V),
      (reducedLaplacian G root).det = (numSpanningTrees G : ℤ)

Sources

• G. Kirchhoff, "Über die Auflösung der Gleichungen, auf welche man bei der Untersuchung der linearen Verteilung galvanischer Ströme geführt wird", Annalen der Physik und Chemie 72 (1847), 497–508, DOI 10.1002/andp.18471481202

Uses 3

Statement usesNumber of spanning trees · Reduced Laplacian

Proof usesMatrix-tree theorem for a chosen root

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.