Kirchhoff's matrix-tree theorem

The determinant of the reduced Laplacian of a finite simple graph, over any integral domain, is the number of its spanning trees. The Cauchy–Binet expansion writes the determinant as a sum of squared maximal minors of the reduced incidence matrix, and each squared minor is 1 exactly when its n - 1 edges form a spanning tree.

Main results

• SimpleGraph.connected_fromEdgeSet_iff_isTree: n - 1 edges span a connected graph iff they form a tree.
• SimpleGraph.det_reducedLapMatrix_eq_card_spanningTrees: det L₀ = #spanning trees.

References

• G. Kirchhoff, Ueber die Auflösung der Gleichungen, auf welche man bei der Untersuchung der linearen Vertheilung galvanischer Ströme geführt wird, Ann. Phys. 148 (1847) 497–508.
• N. Biggs, Algebraic Graph Theory, 2nd ed., Cambridge University Press, 1993, Chapter 6.

theorem SimpleGraph.card_ne_root_add_one {V : Type u_2} [Fintype V] [LinearOrder V] (v₀ : V) : Fintype.card { v : V // v ≠ v₀ } + 1 = Fintype.card V

Deleting one vertex drops the cardinality by exactly one.

theorem SimpleGraph.connected_fromEdgeSet_iff_isTree {V : Type u_2} (G : SimpleGraph V) [Fintype V] [LinearOrder V] (v₀ : V) (S : Finset (Sym2 V)) (hS : S.card = Fintype.card { v : V // v ≠ v₀ }) (hsub : ↑S ⊆ G.edgeSet) : (fromEdgeSet ↑S).Connected ↔ (fromEdgeSet ↑S).IsTree

For a (card V − 1)-set of genuine edges, the spanning subgraph is connected iff it is a tree: the edge count is exactly the tree count, so acyclicity is free.

theorem SimpleGraph.det_reducedLapMatrix_eq_card_spanningTrees (R : Type u_1) {V : Type u_2} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] [IsDomain R] : (reducedLapMatrix R G v₀).det = ↑{S : { s : Finset (Sym2 V) // s.card = Fintype.card { v : V // v ≠ v₀ } } | ↑↑S ⊆ G.edgeSet ∧ (fromEdgeSet ↑↑S).IsTree}.card

Kirchhoff's matrix-tree theorem. Over any integral domain, the determinant of the reduced Laplacian of G (delete the row and column of any root v₀) equals the number of spanning trees of G, counted as the (card V − 1)-subsets of Sym2 V consisting of edges of G that span a tree.