The matching polynomial of a disjoint union

The matchings of a disjoint union G ⊕ H are the pairs of matchings of G and H, so the matching numbers convolve and the matching polynomial is multiplicative. The file also defines the disjoint union of an indexed family of graphs and proves the same multiplicativity for it, together with the transport of vertex deletion along isomorphisms and disjoint unions.

Main definitions

• SimpleGraph.sigmaFamily G: the disjoint union of a family of graphs on Σ i, β i.

Main results

• SimpleGraph.matchingNumber_sum: m_k(G ⊕ H) = ∑_{i + j = k} m_i(G) m_j(H).
• SimpleGraph.matchingPartition_sum, SimpleGraph.matchingPoly_sum: P and μ are multiplicative on G ⊕ H.
• SimpleGraph.matchingPoly_sigmaFamily: μ of an indexed disjoint union is the product.
• SimpleGraph.matchingPoly_true_recurrence: the vertex-deletion recurrence with the vertex removed from the vertex type.

theorem SimpleGraph.mem_edgeSet_sum {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {e : Sym2 (V ⊕ W)} : e ∈ (G ⊕g H).edgeSet ↔ (∃ eV ∈ G.edgeSet, e = Sym2.map Sum.inl eV) ∨ ∃ eW ∈ H.edgeSet, e = Sym2.map Sum.inr eW

Edges of a disjoint sum split. Every edge of G ⊕g H is either the inl-image of an edge of G or the inr-image of an edge of H — there are no cross edges. The combinatorial foundation of the matching convolution.

The matching convolution

def SimpleGraph.combineEdges {V : Type u_3} {W : Type u_4} [DecidableEq V] [DecidableEq W] (a : Finset (Sym2 V)) (b : Finset (Sym2 W)) : Finset (Sym2 (V ⊕ W))

Combine a G-edge finset and an H-edge finset into an edge finset of G ⊕g H, by tagging each side with inl / inr.

Equations

• SimpleGraph.combineEdges a b = Finset.image (Sym2.map Sum.inl) a ∪ Finset.image (Sym2.map Sum.inr) b

theorem SimpleGraph.map_inl_ne_map_inr {V : Type u_3} {W : Type u_4} (eV : Sym2 V) (eW : Sym2 W) : Sym2.map Sum.inl eV ≠ Sym2.map Sum.inr eW

An inl-tagged edge and an inr-tagged edge are never equal.

theorem SimpleGraph.mem_combineEdges {V : Type u_3} {W : Type u_4} [DecidableEq V] [DecidableEq W] {a : Finset (Sym2 V)} {b : Finset (Sym2 W)} {x : Sym2 (V ⊕ W)} : x ∈ combineEdges a b ↔ (∃ eV ∈ a, x = Sym2.map Sum.inl eV) ∨ ∃ eW ∈ b, x = Sym2.map Sum.inr eW

theorem SimpleGraph.card_combineEdges {V : Type u_3} {W : Type u_4} [DecidableEq V] [DecidableEq W] (a : Finset (Sym2 V)) (b : Finset (Sym2 W)) : (combineEdges a b).card = a.card + b.card

The two tagged images are disjoint, so the combined edge finset has additive card.

Vertex-membership of tagged edges

@[simp]

theorem SimpleGraph.inl_mem_map_inl {V : Type u_3} {W : Type u_4} (v : V) (eV : Sym2 V) : Sum.inl v ∈ Sym2.map Sum.inl eV ↔ v ∈ eV

@[simp]

theorem SimpleGraph.inr_mem_map_inr {V : Type u_3} {W : Type u_4} (w : W) (eW : Sym2 W) : Sum.inr w ∈ Sym2.map Sum.inr eW ↔ w ∈ eW

@[simp]

theorem SimpleGraph.inr_notMem_map_inl {V : Type u_3} {W : Type u_4} (w : W) (eV : Sym2 V) : Sum.inr w ∉ Sym2.map Sum.inl eV

@[simp]

theorem SimpleGraph.inl_notMem_map_inr {V : Type u_3} {W : Type u_4} (v : V) (eW : Sym2 W) : Sum.inl v ∉ Sym2.map Sum.inr eW

@[instance_reducible]

noncomputable instance SimpleGraph.instDecidableRelSumAdjSum_formalizations {V : Type u_3} {W : Type u_4} (G : SimpleGraph V) (H : SimpleGraph W) : DecidableRel (G ⊕g H).Adj

Equations

• G.instDecidableRelSumAdjSum_formalizations H x✝¹ x✝ = Classical.propDecidable ((G ⊕g H).Adj x✝¹ x✝)

def SimpleGraph.splitL {V : Type u_3} {W : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) [DecidableRel G.Adj] (s : Finset (Sym2 (V ⊕ W))) : Finset (Sym2 V)

The G-part of an edge set of the sum: the G-edges whose inl-tag lies in s.

Equations

• G.splitL s = {e ∈ G.edgeFinset | Sym2.map Sum.inl e ∈ s}

def SimpleGraph.splitR {V : Type u_3} {W : Type u_4} [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (s : Finset (Sym2 (V ⊕ W))) : Finset (Sym2 W)

The H-part of an edge set of the sum.

Equations

• H.splitR s = {e ∈ H.edgeFinset | Sym2.map Sum.inr e ∈ s}

theorem SimpleGraph.mem_splitL {V : Type u_3} {W : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) [DecidableRel G.Adj] {s : Finset (Sym2 (V ⊕ W))} {eV : Sym2 V} : eV ∈ G.splitL s ↔ eV ∈ G.edgeFinset ∧ Sym2.map Sum.inl eV ∈ s

theorem SimpleGraph.mem_splitR {V : Type u_3} {W : Type u_4} [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {s : Finset (Sym2 (V ⊕ W))} {eW : Sym2 W} : eW ∈ H.splitR s ↔ eW ∈ H.edgeFinset ∧ Sym2.map Sum.inr eW ∈ s

theorem SimpleGraph.combineEdges_subset {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] {a : Finset (Sym2 V)} {b : Finset (Sym2 W)} (ha : a ⊆ G.edgeFinset) (hb : b ⊆ H.edgeFinset) : combineEdges a b ⊆ (G ⊕g H).edgeFinset

theorem SimpleGraph.splitL_combineEdges {V : Type u_3} {W : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) [DecidableRel G.Adj] {a : Finset (Sym2 V)} {b : Finset (Sym2 W)} (ha : a ⊆ G.edgeFinset) : G.splitL (combineEdges a b) = a

theorem SimpleGraph.splitR_combineEdges {V : Type u_3} {W : Type u_4} [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {a : Finset (Sym2 V)} {b : Finset (Sym2 W)} (hb : b ⊆ H.edgeFinset) : H.splitR (combineEdges a b) = b

theorem SimpleGraph.combineEdges_splitL_splitR {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] {s : Finset (Sym2 (V ⊕ W))} (hs : s ⊆ (G ⊕g H).edgeFinset) : combineEdges (G.splitL s) (H.splitR s) = s

theorem SimpleGraph.isMatchingSet_splitL {V : Type u_3} {W : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) [DecidableRel G.Adj] {s : Finset (Sym2 (V ⊕ W))} (hs : IsMatchingSet s) : IsMatchingSet (G.splitL s)

theorem SimpleGraph.isMatchingSet_splitR {V : Type u_3} {W : Type u_4} [Fintype W] [DecidableEq V] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {s : Finset (Sym2 (V ⊕ W))} (hs : IsMatchingSet s) : IsMatchingSet (H.splitR s)

theorem SimpleGraph.isMatchingSet_combineEdges {V : Type u_3} {W : Type u_4} [DecidableEq V] [DecidableEq W] {a : Finset (Sym2 V)} {b : Finset (Sym2 W)} (ha : IsMatchingSet a) (hb : IsMatchingSet b) : IsMatchingSet (combineEdges a b)

theorem SimpleGraph.matchingNumber_sum {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] (k : ℕ) : (G ⊕g H).matchingNumber k = ∑ j ∈ Finset.range (k + 1), G.matchingNumber j * H.matchingNumber (k - j)

The matching convolution. A matching of the disjoint sum splits uniquely into a matching of each part, so the matching numbers convolve: m_k(G ⊕ H) = ∑_{j ≤ k} m_j(G) · m_{k-j}(H).

theorem SimpleGraph.matchingPartition_sum {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] : (G ⊕g H).matchingPartition = G.matchingPartition * H.matchingPartition

Multiplicativity of the monomer–dimer partition function on disjoint unions: P(G ⊕ H) = P(G) · P(H). A clean Cauchy product — the convolution of matching numbers is exactly the coefficient product. (The signless companion of Godsil L25.3.1.)

theorem SimpleGraph.matchingPoly_sum {V : Type u_3} {W : Type u_4} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] : (G ⊕g H).matchingPoly = G.matchingPoly * H.matchingPoly

Multiplicativity of the matching polynomial on disjoint unions (Godsil L25.3.1): μ[G ⊕ H] = μ[G] · μ[H]. Lifts the clean partition multiplicativity matchingPartition_sum through the μ ↔ P bridge matchingPoly_reflect_card: at the common degree the reflection of μ is P ∘ (−X²), and reflecting the product turns it into a reverse, which is multiplicative over the domain ℝ[X] (reverse_mul_of_domain). The Godsil decomposition T_a(G) − a = ⊔_{b∼a} T_b(G−a) then becomes μ[T_a(G) − a] = ∏_{b∼a} μ[T_b(G−a)].

Indexed disjoint union of graphs (the n-ary generalisation of SimpleGraph.sum)

Toward the path-tree root decomposition T(G,u) − r ≅ ⊔_{b∼u} T(G−u, b): we need the disjoint union of a family of graphs and the multiplicativity of μ over it. Mathlib has only the binary SimpleGraph.sum, so we build the Σ-indexed union.

def SimpleGraph.sigmaFamily {ι : Type u_3} {β : ι → Type u_4} (G : (i : ι) → SimpleGraph (β i)) : SimpleGraph ((i : ι) × β i)

The disjoint union of an indexed family of graphs on Σ i, β i: two vertices are adjacent iff they share a fibre i and are adjacent there. (Witness-style, avoiding ▸.)

Equations

• SimpleGraph.sigmaFamily G = { Adj := fun (x y : (i : ι) × β i) => ∃ (i : ι) (a : β i) (b : β i), (G i).Adj a b ∧ x = ⟨i, a⟩ ∧ y = ⟨i, b⟩, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.sigmaFamily_adj {ι : Type u_3} {β : ι → Type u_4} (G : (i : ι) → SimpleGraph (β i)) {i : ι} (a b : β i) : (sigmaFamily G).Adj ⟨i, a⟩ ⟨i, b⟩ ↔ (G i).Adj a b

theorem SimpleGraph.sigmaFamily_not_adj_of_fst_ne {ι : Type u_3} {β : ι → Type u_4} (G : (i : ι) → SimpleGraph (β i)) {x y : (i : ι) × β i} (h : x.fst ≠ y.fst) : ¬(sigmaFamily G).Adj x y

Vertices in different fibres are never adjacent in sigmaFamily.

Option-decomposition: sigmaFamily over Option α is a binary sum

def SimpleGraph.sigmaOptionEquiv {α : Type u_3} {γ : Option α → Type u_4} : (i : Option α) × γ i ≃ γ none ⊕ (a : α) × γ (some a)

The vertex equivalence (Σ i : Option α, γ i) ≃ γ none ⊕ Σ a, γ (some a).

Equations

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

def SimpleGraph.sigmaFamilyOptionIso {α : Type u_3} {γ : Option α → Type u_4} (G : (i : Option α) → SimpleGraph (γ i)) : sigmaFamily G ≃g G none ⊕g sigmaFamily fun (a : α) => G (some a)

sigmaFamily over Option α splits as a binary sum: the none fibre summed with the family over α. The Option-step of the induction proving μ multiplicative over sigmaFamily.

Equations

• SimpleGraph.sigmaFamilyOptionIso G = { toEquiv := SimpleGraph.sigmaOptionEquiv, map_rel_iff' := ⋯ }

def SimpleGraph.sigmaFamilyCongr {α₁ : Type u_5} {α₂ : Type u_6} (e : α₁ ≃ α₂) {γ : α₂ → Type u_7} (G : (i : α₂) → SimpleGraph (γ i)) : (sigmaFamily fun (a : α₁) => G (e a)) ≃g sigmaFamily G

Reindexing sigmaFamily along an equivalence of the index type.

Equations

• SimpleGraph.sigmaFamilyCongr e G = { toEquiv := e.sigmaCongrLeft, map_rel_iff' := ⋯ }

def SimpleGraph.unIsolate {V : Type u_1} [DecidableEq V] (v : V) : { w : V // w ≠ v } ⊕ Unit ≃ V

The equiv ({w ≠ v} ⊕ Unit) ≃ V re-attaching the single vertex v to the rest. A top-level def (not a let/.symm) with @[simp] lemmas keyed on the Sum *constructors, so that after obtain-splitting a sum vertex the applications reduce reliably (a .symm` coe does not).

Equations

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

@[simp]

theorem SimpleGraph.unIsolate_inl {V : Type u_1} [DecidableEq V] (v : V) (w : { w : V // w ≠ v }) : (unIsolate v) (Sum.inl w) = ↑w

@[simp]

theorem SimpleGraph.unIsolate_inr {V : Type u_1} [DecidableEq V] (v : V) (u : Unit) : (unIsolate v) (Sum.inr u) = v

theorem SimpleGraph.matchingPoly_deleteIncidenceSet_isolate {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (v : V) : (G.deleteIncidenceSet v).matchingPoly = (induce {w : V | w ≠ v} G).matchingPoly * Polynomial.X

Isolated-vertex bridge (route A). μ(G − v) = μ(G⟦≠v⟧) · X. Deleting v's incidences leaves v isolated, so G.deleteIncidenceSet v ≅g (G.induce {w ≠ v}) ⊕ (⊥ on a point); μ of an isolated point is X. Relates the fixed-n deletion (same vertex type, what matchingPoly_recurrence uses) to the genuine induced subgraph (variable degree, what hl_geom_recurrence consumes).

def SimpleGraph.unIsolate₂ {V : Type u_1} [DecidableEq V] (v t : V) (htv : t ≠ v) : ({ w : V // w ≠ v ∧ w ≠ t } ⊕ Unit) ⊕ Unit ≃ V

The equiv ((({≠v,≠t}) ⊕ Unit) ⊕ Unit) ≃ V re-attaching the two distinct vertices v, t.

Equations

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

theorem SimpleGraph.matchingPoly_deleteIncidenceSet_isolate₂ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {v t : V} (htv : t ≠ v) : ((G.deleteIncidenceSet v).deleteIncidenceSet t).matchingPoly = (induce {w : V | w ≠ v ∧ w ≠ t} G).matchingPoly * Polynomial.X ^ 2

Two-vertex isolation (route A, double step). μ((G−v)−t) = μ(G⟦≠v,≠t⟧)·X² for t ≠ v.

theorem SimpleGraph.matchingPoly_true_recurrence {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (v : V) : G.matchingPoly = Polynomial.X * (induce {w : V | w ≠ v} G).matchingPoly - ∑ u ∈ G.neighborFinset v, (induce {w : V | w ≠ v ∧ w ≠ u} G).matchingPoly

True (variable-degree) matching recurrence (Godsil / Spielman L25.3.2). μ(G) = X·μ(G⟦≠v⟧) − Σ_{u∼v} μ(G⟦≠v,≠u⟧), deletions being genuine induced subgraphs. Obtained from the X²-padded fixed-n matchingPoly_recurrence by substituting the isolated-vertex bridges (μ(G−v)=X·μ(G⟦≠v⟧), μ((G−v)−u)=X²·μ(G⟦≠v,≠u⟧)) and cancelling X² (ℝ[X] is a domain). This is the recurrence the geometric Heilmann–Lieb induction (hl_geom_recurrence) consumes.

theorem SimpleGraph.matchingPoly_induce_induce {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (a b : V) : (induce {x : ↑{w : V | w ≠ a} | ↑x ≠ b} (induce {w : V | w ≠ a} G)).matchingPoly = (induce {w : V | w ≠ a ∧ w ≠ b} G).matchingPoly

Induce-of-induce = induce-of-intersection (for μ). μ((G⟦≠a⟧)⟦≠b⟧) = μ(G⟦≠a,≠b⟧). Lets the recurrence's second-deletion terms μ(G⟦≠a,≠b⟧) be read as one-step deletions of the induced subgraph G⟦≠a⟧, so the induction hypothesis on G⟦≠a⟧ (fewer vertices) applies to them. The vertex equiv is Equiv.subtypeSubtypeEquivSubtypeInter; adjacency is definitional (induce_adj is rfl).

Vertex deletion through isomorphisms and disjoint unions

For Godsil's identity () we apply the vertex-deletion recurrence to the path tree at its root and must evaluate μ(T − r − c) for each child c. Transporting through rootDecompIso, that is deleting one more vertex inside one component of (⊥ Unit) ⊕ ⊔_b T(G−u,b). These three isos do the bookkeeping: deletion commutes with any iso, deleting a right-summand only touches the right graph, and deleting a vertex of one sigmaFamily fibre only touches that fibre.

def SimpleGraph.Iso.deleteIncidenceSet {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (v : V) : G.deleteIncidenceSet v ≃g H.deleteIncidenceSet (e v)

A graph isomorphism transports incidence deletion: deleting v from G is isomorphic to deleting e v from H, with the same vertex map e.

Equations

• e.deleteIncidenceSet v = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }

theorem SimpleGraph.matchingPoly_deleteIncidenceSet_iso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] [DecidableRel G.Adj] [DecidableRel H.Adj] (e : G ≃g H) (v : V) : (G.deleteIncidenceSet v).matchingPoly = (H.deleteIncidenceSet (e v)).matchingPoly

μ transports through an iso composed with one incidence deletion. A general lemma: μ(G−v) = μ(H−(e v)). Proving it once for an abstract e keeps matchingPoly_iso's matchingNumber_iso/whnf work over the deleted graph abstract; applying it to a concrete complex iso (e.g. rootDecompIso) is then a pure instantiation, dodging the whnf blow-up that matchingPoly_iso (e.deleteIncidenceSet v) triggers inline on a doubly-deleted Σ-graph.

def SimpleGraph.sumDeleteIncidenceSetInr {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) (y : W) : (G ⊕g H).deleteIncidenceSet (Sum.inr y) ≃g G ⊕g H.deleteIncidenceSet y

Deleting a right-summand vertex Sum.inr y from G ⊕g H only touches H.

Equations

• G.sumDeleteIncidenceSetInr H y = { toEquiv := Equiv.refl (V ⊕ W), map_rel_iff' := ⋯ }

def SimpleGraph.sigmaFamilyDeleteIncidenceSet {ι : Type u_3} [DecidableEq ι] {β : ι → Type u_4} (G : (i : ι) → SimpleGraph (β i)) (b : ι) (y : β b) : (sigmaFamily G).deleteIncidenceSet ⟨b, y⟩ ≃g sigmaFamily (Function.update G b ((G b).deleteIncidenceSet y))

Deleting a vertex ⟨b, y⟩ of one fibre b from sigmaFamily G only touches that fibre: the result is sigmaFamily with G b replaced by (G b).deleteIncidenceSet y.

Equations

• SimpleGraph.sigmaFamilyDeleteIncidenceSet G b y = { toEquiv := Equiv.refl ((i : ι) × β i), map_rel_iff' := ⋯ }

μ is multiplicative over the indexed disjoint union

theorem SimpleGraph.matchingPoly_sigmaFamily {ι : Type u} [Fintype ι] {β : ι → Type v} [(i : ι) → Fintype (β i)] (G : (i : ι) → SimpleGraph (β i)) : (sigmaFamily G).matchingPoly = ∏ i : ι, (G i).matchingPoly

μ[sigmaFamily G] = ∏ μ[G i] over a finite index — the product the path-tree root decomposition needs. Proved by induction on n = |ι| over Fin n (so all Fintypes are the canonical Fin/Option/⊕ ones — avoiding the Fintype.ofEquiv diamond that makes the direct Fintype.induction_empty_option route diverge in whnf), then transported to a general index by one equivFin reindex. The successor step is matchingPoly_sum through sigmaFamilyOptionIso after finSuccEquiv; the transport is matchingPoly_iso through sigmaFamilyCongr + Equiv.prod_comp.