The reduced Laplacian and its Cauchy–Binet expansion

Deleting the row of a root vertex v₀ from the oriented incidence matrix N of a simple graph gives the reduced incidence matrix N₀, and N₀ N₀ᵀ is the reduced Laplacian L₀ (the Laplacian with the row and column of v₀ removed). By the Cauchy–Binet formula, det L₀ is the sum of the squares of the maximal minors of N₀.

Main definitions

• SimpleGraph.reducedIncMatrix G R v₀, SimpleGraph.reducedLapMatrix G R v₀.

Main results

• SimpleGraph.reducedLapMatrix_eq_mul_transpose: L₀ = N₀ N₀ᵀ.
• SimpleGraph.det_reducedLapMatrix_eq_sum_sq: det L₀ = ∑_S det(N₀[S])² over the (n - 1)-subsets S of Sym2 V.

@[instance_reducible]

def SimpleGraph.sym2LinearOrder {V : Type u_1} [LinearOrder V] : LinearOrder (Sym2 V)

Linear order on unordered pairs, via the lexicographic order on (inf, sup). Scoped: this is just the indexing device Cauchy–Binet needs, not a canonical structure.

Equations

• SimpleGraph.sym2LinearOrder = LinearOrder.lift' (fun (e : Sym2 V) => toLex (e.inf, e.sup)) ⋯

def SimpleGraph.reducedIncMatrix (R : Type u_1) {V : Type u_2} (G : SimpleGraph V) [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [Zero R] [One R] [Neg R] : Matrix { v : V // v ≠ v₀ } (Sym2 V) R

The reduced oriented incidence matrix: delete the row of the root v₀.

Equations

• SimpleGraph.reducedIncMatrix R G v₀ = (SimpleGraph.orientedIncMatrix R G).submatrix Subtype.val id

def SimpleGraph.reducedLapMatrix (R : Type u_1) {V : Type u_2} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [AddGroupWithOne R] : Matrix { v : V // v ≠ v₀ } { v : V // v ≠ v₀ } R

The reduced Laplacian: delete row and column of the root v₀.

Equations

• SimpleGraph.reducedLapMatrix R G v₀ = (SimpleGraph.lapMatrix R G).submatrix Subtype.val Subtype.val

theorem SimpleGraph.reducedLapMatrix_eq_mul_transpose {R : Type u_1} {V : Type u_2} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [Ring R] : reducedLapMatrix R G v₀ = reducedIncMatrix R G v₀ * (reducedIncMatrix R G v₀).transpose

Lemma 1 restricted: the reduced Laplacian is the Gram matrix of the reduced oriented incidence matrix.

theorem SimpleGraph.det_reducedLapMatrix_eq_sum_sq {R : Type u_1} {V : Type u_2} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] : (reducedLapMatrix R G v₀).det = ∑ S : { s : Finset (Sym2 V) // s.card = Fintype.card { v : V // v ≠ v₀ } }, ((reducedIncMatrix R G v₀).submatrix ⇑(Fintype.equivFin { v : V // v ≠ v₀ }).symm ⇑((↑S).orderEmbOfFin ⋯)).det ^ 2

Sum-of-squared-minors identity. Cauchy–Binet applied to L₀ = N₀ * N₀ᵀ: the determinant of the reduced Laplacian is the sum, over all (card V − 1)-subsets S of Sym2 V, of the square of the maximal minor of N₀ with columns S.