Connected components and path-tree divisibility

The matching polynomial of a graph is the product of those of its connected components, and the matching polynomial of the path tree at w only depends on the component of w. With Godsil's identity this gives the divisibility μ(G) ∣ μ(T(G, u)) for connected G, by induction on the number of vertices.

Main results

• SimpleGraph.matchingPoly_eq_prod_components: μ(G) = ∏_C μ(G[C]) over connected components.
• SimpleGraph.matchingPoly_pathTree_eq_induce_component: the path tree at w has the same matching polynomial as the path tree of the component of w.
• SimpleGraph.connected_matchingPoly_dvd_pathTree: μ(G) ∣ μ(T(G, u)) for connected G.

References

• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.

def SimpleGraph.componentDecompEquiv {V : Type u_1} (G : SimpleGraph V) : V ≃ (C : G.ConnectedComponent) × ↑C.supp

The vertex equivalence V ≃ Σ C : ConnectedComponent, ↥C.supp (every vertex lies in exactly one component; C.supp = {v | mk v = C} is the fibre of connectedComponentMk over C).

Equations

• G.componentDecompEquiv = { toFun := fun (v : V) => ⟨G.connectedComponentMk v, ⟨v, ⋯⟩⟩, invFun := fun (x : (C : G.ConnectedComponent) × ↑C.supp) => ↑x.snd, left_inv := ⋯, right_inv := ⋯ }

def SimpleGraph.componentDecompIso {V : Type u_1} (G : SimpleGraph V) : G ≃g sigmaFamily fun (C : G.ConnectedComponent) => induce C.supp G

G is the disjoint union of its component-induced subgraphs. The decomposition graph isomorphism G ≃g ⊔_C G⟦C.supp⟧: adjacency only ever occurs within a single component (connectedComponentMk_eq_of_adj), where it is the induced adjacency.

Equations

• G.componentDecompIso = { toEquiv := G.componentDecompEquiv, map_rel_iff' := ⋯ }

theorem SimpleGraph.matchingPoly_eq_prod_components {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingPoly = ∏ C : G.ConnectedComponent, (induce C.supp G).matchingPoly

The matching polynomial is multiplicative over connected components.

theorem SimpleGraph.exists_adj_reachable_of_ne {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (hG : G.Connected) {u w : V} (hw : w ≠ u) : ∃ (b : V), G.Adj u b ∧ (G.deleteIncidenceSet u).Reachable b w

On a connected graph, every vertex w ≠ u has a u-neighbour reachable to it in G − u (i.e. its G − u connected component contains a neighbour of u). A path u → w (connected) begins with an edge u → b; its tail is a path avoiding u, hence a walk in G − u from b to w. This is the lemma that, in the path-tree divisibility, attaches each non-u component of G − u to a child subtree T(G−u, b).

Path-tree confinement to a component (lemma c)

def SimpleGraph.Walk.toInduce {V : Type u_2} {H : SimpleGraph V} {s : Set V} {w x : V} (hw : w ∈ s) (hx : x ∈ s) (p : H.Walk w x) : (∀ y ∈ p.support, y ∈ s) → (induce s H).Walk ⟨w, hw⟩ ⟨x, hx⟩

Transport a walk into an induced subgraph. A walk of H whose support lies in s becomes a walk of H.induce s between the corresponding subtype endpoints.

Equations

• SimpleGraph.Walk.toInduce x_1 x_8 SimpleGraph.Walk.nil x_9 = SimpleGraph.Walk.nil
• SimpleGraph.Walk.toInduce x_2 x_3 (SimpleGraph.Walk.cons h q) hsupp = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toInduce ⋯ x_3 q ⋯)

theorem SimpleGraph.Walk.map_toInduce {V : Type u_2} {H : SimpleGraph V} {s : Set V} {w x : V} (hw : w ∈ s) (hx : x ∈ s) (p : H.Walk w x) (hsupp : ∀ y ∈ p.support, y ∈ s) : Walk.map (Embedding.induce s).toHom (toInduce hw hx p hsupp) = p

Mapping a transported walk back through the induced-subgraph embedding recovers the original.

theorem SimpleGraph.Walk.toInduce_map {V : Type u_2} {H : SimpleGraph V} {s : Set V} {a b : ↑s} (p : (induce s H).Walk a b) (hsupp : ∀ y ∈ (Walk.map (Embedding.induce s).toHom p).support, y ∈ s) : toInduce ⋯ ⋯ (Walk.map (Embedding.induce s).toHom p) hsupp = p

Lifting a walk that was mapped down from H.induce s recovers it (the other roundtrip).

theorem SimpleGraph.Walk.toInduce_isPath {V : Type u_2} {H : SimpleGraph V} {s : Set V} {w x : V} (hw : w ∈ s) (hx : x ∈ s) (p : H.Walk w x) (hsupp : ∀ y ∈ p.support, y ∈ s) (hp : p.IsPath) : (toInduce hw hx p hsupp).IsPath

The transported walk is a path when the original is (its support is unchanged).

theorem SimpleGraph.Walk.mem_component_supp_of_mem_support {V : Type u_2} {H : SimpleGraph V} [DecidableEq V] {w x : V} (p : H.Walk w x) {y : V} (hy : y ∈ p.support) : y ∈ (H.connectedComponentMk w).supp

Every vertex on a walk starting at w lies in w's connected component.

theorem SimpleGraph.Walk.map_concat {V₁ : Type u_3} {V₂ : Type u_4} {G₁ : SimpleGraph V₁} {G₂ : SimpleGraph V₂} (f : G₁ →g G₂) {u v z : V₁} (p : G₁.Walk u v) (h : G₁.Adj v z) : Walk.map f (p.concat h) = (Walk.map f p).concat ⋯

map commutes with concat (appending one edge).

The confinement bijection on path-tree vertices

noncomputable def SimpleGraph.pathTreeComponentEquiv {V : Type u_1} [DecidableEq V] (H : SimpleGraph V) (w : V) : (induce (H.connectedComponentMk w).supp H).PathFrom ⟨w, ⋯⟩ ≃ H.PathFrom w

Confinement vertex bijection. Paths of H from w correspond to paths of the component-induced subgraph H.induce (comp w).supp from ⟨w, _⟩: a path of H from w stays in w's component, so it transports (both ways) across the induced-subgraph embedding. Forward = Path.mapEmbedding; injective by mapEmbedding_injective; surjective by the lift Walk.toInduce (with map_toInduce the roundtrip).

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.matchingPoly_pathTree_eq_induce_component {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (w : V) : (H.pathTree w).matchingPoly = ((induce (H.connectedComponentMk w).supp H).pathTree ⟨w, ⋯⟩).matchingPoly

Path-tree confinement (lemma c). The matching polynomial of the path tree from w depends only on w's connected component: μ(T(H,w)) = μ(T(H⟦comp w⟧, w)). Proof: the vertex bijection pathTreeComponentEquiv is a graph isomorphism of path trees — it preserves the Grows (extend-by-one-edge) relation because Path.mapEmbedding commutes with concat (map_concat) and the embedding is injective — so matchingPoly_iso applies. This is the input the path-tree divisibility needs: in (D), the child subtree T(G−u, b) (for b in component C) has the same μ as T(C, b), where the inductive hypothesis applies.

the path-tree divisibility assembly

theorem SimpleGraph.matchingPoly_induce_supp_congr {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] {C C' : H.ConnectedComponent} (h : C = C') : (induce C.supp H).matchingPoly = (induce C'.supp H).matchingPoly

μ(H⟦C.supp⟧) depends only on the component C — a congruence used to bridge a component named via a representative (comp b) with the same component appearing as a product index. Proven by subst so as to never rw the set inside induce/matchingPoly (the DecidableRel-motive trap documented for lemma (c)/Lemma A).

theorem SimpleGraph.matchingPoly_induce_isolated_component {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (u : V) (hiso : ∀ (c : V), ¬H.Adj u c) : (induce (H.connectedComponentMk u).supp H).matchingPoly = Polynomial.X

Lemma A. When u is isolated in H (no H-neighbours), its connected component is the singleton {u}, the induced subgraph is edgeless, and μ(H⟦comp u⟧) = X. Proven without rewriting the graph inside μ (the DecidableRel-motive trap): a walk out of an isolated u must be nil, so comp u is a subsingleton; build the identity iso to ⊥ on the (subsingleton) carrier and evaluate matchingPoly_bot at card 1.

theorem SimpleGraph.connected_matchingPoly_dvd_pathTree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (u : V) : G.matchingPoly ∣ (G.pathTree u).matchingPoly

path-tree divisibility (connected case). μ(G) ∣ μ(T(G,u)) for every connected finite graph (matchingPoly_dvd_pathTree_aux specialized to |V|). The final specialization is bridged by matchingPoly_inst_irrel rather than exact, so isDefEq never has to structurally compare the Fintype (PathFrom)/DecidableRel (pathTree.Adj) instances of the goal against the generalized statement (a whnf blow-up over the Σ-of-paths type).