Maximal minors of the reduced incidence matrix

For an (n - 1)-subset S of Sym2 V, the square of the maximal minor of the reduced incidence matrix selected by S is 1 if the edges of S are edges of G and form a connected spanning subgraph, and 0 otherwise. In the connected case the minor is made triangular by ordering the vertices by distance to the root and matching each vertex with the edge to its parent, so the minor is ±1; otherwise a column is zero or the rows of a component away from the root sum to zero.

Main definitions

• SimpleGraph.treeParent, SimpleGraph.parentEdge: a parent of each non-root vertex, one step closer to the root, and the corresponding edge.

Main results

• SimpleGraph.det_minor_eq_zero_of_not_subset_edgeSet, SimpleGraph.det_minor_eq_zero_of_not_connected: the vanishing cases.
• SimpleGraph.sq_det_minor_eq_one_of_connected: the connected case.
• SimpleGraph.sq_det_minor_eq_ite: the dichotomy.

theorem SimpleGraph.Connected.exists_adj_dist_succ {V : Type u_1} {H : SimpleGraph V} {v₀ : V} (hconn : H.Connected) {u : V} (hu : u ≠ v₀) : ∃ (w : V), H.Adj u w ∧ H.dist w v₀ + 1 = H.dist u v₀

Every non-root vertex of a connected graph has a neighbour strictly closer to the root: the second vertex of a geodesic walk to the root.

noncomputable def SimpleGraph.treeParent {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) (u : { v : V // v ≠ v₀ }) : V

The parent of a non-root vertex: a fixed neighbour strictly closer to the root.

Equations

• SimpleGraph.treeParent v₀ hconn u = ⋯.choose

theorem SimpleGraph.treeParent_adj {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) (u : { v : V // v ≠ v₀ }) : H.Adj (↑u) (treeParent v₀ hconn u)

theorem SimpleGraph.treeParent_dist {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) (u : { v : V // v ≠ v₀ }) : H.dist (treeParent v₀ hconn u) v₀ + 1 = H.dist (↑u) v₀

noncomputable def SimpleGraph.parentEdge {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) (u : { v : V // v ≠ v₀ }) : Sym2 V

The parent edge of a non-root vertex.

Equations

• SimpleGraph.parentEdge v₀ hconn u = s(↑u, SimpleGraph.treeParent v₀ hconn u)

theorem SimpleGraph.parentEdge_mem_edgeSet {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) (u : { v : V // v ≠ v₀ }) : parentEdge v₀ hconn u ∈ H.edgeSet

theorem SimpleGraph.parentEdge_injective {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) : Function.Injective (parentEdge v₀ hconn)

Distance arithmetic kills the swap case: the parent-edge map is injective.

theorem SimpleGraph.eq_or_dist_lt_of_mem_parentEdge {V : Type u_1} {H : SimpleGraph V} (v₀ : V) (hconn : H.Connected) {x : V} {w : { v : V // v ≠ v₀ }} (hx : x ∈ parentEdge v₀ hconn w) : x = ↑w ∨ H.dist x v₀ < H.dist (↑w) v₀

Membership of a vertex in a parent edge pins it down: the vertex itself, or the parent (which is strictly closer to the root).

Part B — the degenerate cases: det = 0

(a) a non-edge in S gives a zero column; (b) if fromEdgeSet S is disconnected, the rows of a component avoiding the root sum to zero.

theorem SimpleGraph.det_minor_eq_zero_of_not_subset_edgeSet (R : Type u_2) {V : Type u_3} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] (S : Finset (Sym2 V)) (hS : S.card = Fintype.card { v : V // v ≠ v₀ }) (hx : ¬↑S ⊆ G.edgeSet) : ((reducedIncMatrix R G v₀).submatrix ⇑(Fintype.equivFin { v : V // v ≠ v₀ }).symm ⇑(S.orderEmbOfFin hS)).det = 0

Case (a). A (card V − 1)-subset containing a non-edge has a zero column in the reduced incidence minor, so the minor is singular.

theorem SimpleGraph.det_minor_eq_zero_of_not_connected (R : Type u_2) {V : Type u_3} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] [IsDomain R] (S : Finset (Sym2 V)) (hS : S.card = Fintype.card { v : V // v ≠ v₀ }) (hsub : ↑S ⊆ G.edgeSet) (hdis : ¬(fromEdgeSet ↑S).Connected) : ((reducedIncMatrix R G v₀).submatrix ⇑(Fintype.equivFin { v : V // v ≠ v₀ }).symm ⇑(S.orderEmbOfFin hS)).det = 0

Case (b). If the spanning subgraph on S is disconnected, some component misses the root; its rows sum to zero, so the reduced incidence minor is singular.

Part C — the connected case: det² = 1

Recolumn the minor by the parent-edge bijection and sort by the key (dist · v₀, ·): the result is upper-triangular with ±1 diagonal. No acyclicity needed — connectivity plus the edge count do all the work (and force fromEdgeSet S to be a spanning tree a posteriori).

theorem SimpleGraph.sq_det_minor_eq_one_of_connected (R : Type u_2) {V : Type u_3} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] (S : Finset (Sym2 V)) (hS : S.card = Fintype.card { v : V // v ≠ v₀ }) (hsub : ↑S ⊆ G.edgeSet) (hconn : (fromEdgeSet ↑S).Connected) : ((reducedIncMatrix R G v₀).submatrix ⇑(Fintype.equivFin { v : V // v ≠ v₀ }).symm ⇑(S.orderEmbOfFin hS)).det ^ 2 = 1

Case (c). If S consists of card V − 1 genuine edges spanning a connected graph, the reduced incidence minor has determinant ±1.

Lemma 3 — the dichotomy, packaged for Lemma 4

theorem SimpleGraph.sq_det_minor_eq_ite (R : Type u_2) {V : Type u_3} (G : SimpleGraph V) [Fintype V] [LinearOrder V] [DecidableRel G.Adj] (v₀ : V) [CommRing R] [IsDomain R] (S : Finset (Sym2 V)) (hS : S.card = Fintype.card { v : V // v ≠ v₀ }) : ((reducedIncMatrix R G v₀).submatrix ⇑(Fintype.equivFin { v : V // v ≠ v₀ }).symm ⇑(S.orderEmbOfFin hS)).det ^ 2 = if ↑S ⊆ G.edgeSet ∧ (fromEdgeSet ↑S).Connected then 1 else 0

The spanning-tree minor dichotomy. The squared maximal minor of the reduced oriented incidence matrix is 1 when S spans a connected subgraph of genuine edges (with card V − 1 of them, a spanning tree), and 0 otherwise.