Reconstruction Conjecture — Disconnected Graphs

Kelly (1942) proved that disconnected graphs are reconstructible: if G is disconnected and has the same deck as H, then G ≅ H.

Main results

• SimpleGraph.isoSigmaComponents — every graph is isomorphic to the disjoint union of its connected components (via a Sigma type).
• SimpleGraph.componentSigmaGraphIsoOfComponentIso — componentwise isomorphisms assemble into an isomorphism between the Sigma component graphs.
• SimpleGraph.isoOfComponentIsoEquiv — if the connected components of two graphs are matched by isomorphism, then the graphs themselves are isomorphic.
• SimpleGraph.isoOfComponentCountEq — if every component isomorphism class occurs equally often in two graphs, then the graphs are isomorphic.
• SimpleGraph.SameDeck.componentCount_eq_components_of_not_connected — the triangular component-multiset recovery induction for same-deck disconnected graphs.
• SimpleGraph.SameDeck.card_isolated_eq — the number of isolated vertices (degree-0 vertices, equivalently the number of K₁ components) is reconstructible. This is the base case of Kelly's 1942 multiset-recovery induction.
• SimpleGraph.SameDeck.iso_of_not_connected — disconnected graphs are reconstructible.

Proof outline for the main theorem

If G is disconnected with connected components of sizes n₁ ≥ n₂ ≥ ⋯ ≥ nₖ where k ≥ 2:

1. Since k ≥ 2, every component has size ≤ n - 1 < n, so Kelly's Lemma applies to every component of G.
2. One can therefore count, for each iso-class [F] of connected graphs on < n vertices, the number of induced copies of F in G.
3. The number of components of G isomorphic to each such F is then recoverable by induction on component size: the smallest components are counted directly (e.g. isolated vertices correspond to degree-0 vertices); larger component classes are obtained by subtracting contributions of induced F-copies lying inside larger components (processed in order).
4. Since G and H have matching component multisets, one constructs a bijection between G.ConnectedComponent and H.ConnectedComponent respecting iso-class, then assembles a global iso G ≃g H by combining per-component isos through the Sigma decomposition (isoSigmaComponents below).

Current status

This file provides the Sigma-decomposition infrastructure (componentSigmaGraph, isoSigmaComponents), the componentwise assembly theorem isoOfComponentIsoEquiv, and the final packaging theorem SameDeck.iso_of_not_connected. The triangular multiset-reconstruction induction itself lives in Reconstruction.Disconnected.ComponentCount.

References

• Kelly, P. J. (1942). "On isometric transformations".

Sigma decomposition of a graph by connected components

Given G : SimpleGraph V, we build an isomorphism G ≃g componentSigmaGraph G where the right-hand side lives on Σ c : G.ConnectedComponent, c.supp and places an edge between ⟨c, v⟩ and ⟨d, w⟩ iff c = d and G.Adj v w.

This is the natural "disjoint-union" description of G in terms of its connected components; it is the structural step needed when assembling a global isomorphism out of per-component isomorphisms.

def SimpleGraph.componentSigmaGraph {V : Type u_1} (G : SimpleGraph V) : SimpleGraph ((c : G.ConnectedComponent) × ↑↑c)

The disjoint-union of the connected components of G, as a graph on the Sigma type Σ c : G.ConnectedComponent, c.supp. Two vertices are adjacent iff they lie in the same component and are adjacent in G.

Equations

• G.componentSigmaGraph = { Adj := fun (p q : (c : G.ConnectedComponent) × ↑↑c) => p.fst = q.fst ∧ G.Adj ↑p.snd ↑q.snd, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.componentSigmaGraph_adj {V : Type u_1} (G : SimpleGraph V) (p q : (c : G.ConnectedComponent) × ↑↑c) : G.componentSigmaGraph.Adj p q ↔ p.fst = q.fst ∧ G.Adj ↑p.snd ↑q.snd

def SimpleGraph.componentSigmaEquiv {V : Type u_1} (G : SimpleGraph V) : V ≃ (c : G.ConnectedComponent) × ↑↑c

The vertex equivalence underlying the Sigma decomposition.

Equations

• G.componentSigmaEquiv = { toFun := SimpleGraph.vToSigma✝ G, invFun := SimpleGraph.sigmaToV✝ G, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SimpleGraph.componentSigmaEquiv_apply {V : Type u_1} (G : SimpleGraph V) (v : V) : G.componentSigmaEquiv v = ⟨G.connectedComponentMk v, ⟨v, ⋯⟩⟩

@[simp]

theorem SimpleGraph.componentSigmaEquiv_symm_apply {V : Type u_1} (G : SimpleGraph V) (p : (c : G.ConnectedComponent) × ↑↑c) : G.componentSigmaEquiv.symm p = ↑p.snd

def SimpleGraph.isoSigmaComponents {V : Type u_1} (G : SimpleGraph V) : G ≃g G.componentSigmaGraph

Sigma decomposition of a graph. Every graph is isomorphic to the disjoint union of its connected components (presented as a Sigma-indexed collection of vertex sets with the induced adjacency).

Equations

• G.isoSigmaComponents = { toEquiv := G.componentSigmaEquiv, map_rel_iff' := ⋯ }

Assembling componentwise isomorphisms

noncomputable def SimpleGraph.componentSigmaGraphIsoOfComponentIso {V : Type u_1} {G H : SimpleGraph V} (e : G.ConnectedComponent ≃ H.ConnectedComponent) (hiso : ∀ (c : G.ConnectedComponent), Nonempty (induce c.supp G ≃g induce (e c).supp H)) : G.componentSigmaGraph ≃g H.componentSigmaGraph

A matching of connected components, together with graph isomorphisms on each matched pair of component-induced subgraphs, induces an isomorphism between the Sigma presentations of the two graphs.

Equations

• SimpleGraph.componentSigmaGraphIsoOfComponentIso e hiso = { toEquiv := e.sigmaCongr fun (c : G.ConnectedComponent) => ⋯.some.toEquiv, map_rel_iff' := ⋯ }

theorem SimpleGraph.isoOfComponentIsoEquiv {V : Type u_1} {G H : SimpleGraph V} (e : G.ConnectedComponent ≃ H.ConnectedComponent) (hiso : ∀ (c : G.ConnectedComponent), Nonempty (induce c.supp G ≃g induce (e c).supp H)) : Nonempty (G ≃g H)

If the connected components of G and H can be bijected so that matched component-induced subgraphs are isomorphic, then G and H are isomorphic.

This is the formal assembly step in Kelly's disconnected-graph reconstruction argument: once the component multiset has been recovered, the global graph isomorphism follows by transporting through the Sigma component decompositions.

Data-carrying component assembly

A variant of componentSigmaGraphIsoOfComponentIso / isoOfComponentIsoEquiv that takes the per-component isomorphisms as data (not merely Nonempty) and exposes the assembled isomorphism's action vertex by vertex (componentIso_apply). Separator reconstruction needs this: to check that an assembled card isomorphism preserves a deleted vertex's link, one must know how it acts on each vertex, and the Nonempty-based assembly discards that.

def SimpleGraph.componentSigmaGraphIso {V : Type u_1} {G H : SimpleGraph V} (e : G.ConnectedComponent ≃ H.ConnectedComponent) (ι : (c : G.ConnectedComponent) → induce c.supp G ≃g induce (e c).supp H) : G.componentSigmaGraph ≃g H.componentSigmaGraph

Data version of componentSigmaGraphIsoOfComponentIso: assemble the Sigma isomorphism from given per-component isomorphisms.

Equations

• SimpleGraph.componentSigmaGraphIso e ι = { toEquiv := e.sigmaCongr fun (c : G.ConnectedComponent) => (ι c).toEquiv, map_rel_iff' := ⋯ }

def SimpleGraph.componentIso {V : Type u_1} {G H : SimpleGraph V} (e : G.ConnectedComponent ≃ H.ConnectedComponent) (ι : (c : G.ConnectedComponent) → induce c.supp G ≃g induce (e c).supp H) : G ≃g H

Data version of isoOfComponentIsoEquiv: a component bijection together with per-component isomorphisms assembles into a global isomorphism G ≃g H.

Equations

• SimpleGraph.componentIso e ι = RelIso.trans G.isoSigmaComponents (RelIso.trans (SimpleGraph.componentSigmaGraphIso e ι) H.isoSigmaComponents.symm)

theorem SimpleGraph.componentIso_apply {V : Type u_1} {G H : SimpleGraph V} (e : G.ConnectedComponent ≃ H.ConnectedComponent) (ι : (c : G.ConnectedComponent) → induce c.supp G ≃g induce (e c).supp H) (x : V) : (componentIso e ι) x = ↑((ι (G.connectedComponentMk x)) ⟨x, ⋯⟩)

The assembled isomorphism acts on a vertex x via the isomorphism of the component containing x.

theorem SimpleGraph.isoOfComponentCountEq {V : Type u_1} [Fintype V] {G H : SimpleGraph V} (hGcount : ∀ (c : G.ConnectedComponent), (induce c.supp G).componentCount G = (induce c.supp G).componentCount H) (hHcount : ∀ (d : H.ConnectedComponent), (induce d.supp H).componentCount G = (induce d.supp H).componentCount H) : Nonempty (G ≃g H)

If every connected-component isomorphism class has the same multiplicity in G and H, then G and H are isomorphic.

This packages the final two steps of Kelly's disconnected-graph argument: component-count equality gives a component bijection preserving isomorphism classes (componentEquivOfComponentCountEq), and the Sigma decomposition then assembles those component isomorphisms into a global graph isomorphism.

Main theorem

theorem SimpleGraph.SameDeck.card_isolated_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : {v : V | G.degree v = 0}.card = {v : V | H.degree v = 0}.card

The number of isolated vertices is reconstructible.

If G and H have the same deck on ≥ 3 vertices, then they have the same number of degree-0 vertices. This is the base case of Kelly's 1942 multiset-recovery induction: a vertex has degree 0 iff its connected component is a single isolated vertex (a K₁ component), so this counts the number of K₁ components as well.

The proof transports the G-side degree-0 filter across the bijection σ : V ≃ V from SameDeck.degree_eq, using that σ preserves degrees.

theorem SimpleGraph.SameDeck.iso_of_not_connected {V : Type u_1} [Fintype V] {G H : SimpleGraph V} (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) (hdisc : ¬G.Connected) : Nonempty (G ≃g H)

Disconnected graphs are reconstructible (Kelly 1942).

If G is disconnected (not connected) and has the same deck as H on ≥ 3 vertices, then G ≅ H.

The proof uses the triangular component-count induction from SameDeck.componentCount_eq_components_of_not_connected, then assembles the matched component multiset with isoOfComponentCountEq.