Documentation

Reconstruction.ConnectedComponents

Reconstruction Conjecture — Connected Components #

The number of connected components and the property of being connected are reconstructible graph invariants.

Main results #

References #

source
def SimpleGraph.numComponents {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) :
ℕ

The number of connected components of a graph.

Equations
Instances For
    source
    theorem SimpleGraph.SameDeck.connected {V : Type u_1} [Fintype V] {G H : SimpleGraph V} (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) (hconn : G.Connected) :
    H.Connected

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

    The proof finds a non-cut vertex v in G (which exists in any connected graph on ≥ 2 vertices). The deck isomorphism gives G - v ≅ H - σ(v), so H - σ(v) is connected. Since every vertex of H has positive degree (degree sequence is reconstructible), σ(v) has a neighbor in H, and we can extend connectivity of H - σ(v) to all of H.

    source
    theorem SimpleGraph.SameDeck.numComponents_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) :
    G.numComponents = H.numComponents

    The number of connected components is reconstructible.

    The proof proceeds by cases:

    • Connected case: both graphs have 1 component (by SameDeck.connected).
    • Isolated vertex case: if some vertex has degree 0, use the fact that removing an isolated vertex drops the component count by 1, while removing a non-isolated vertex can only increase it. The deck gives c(G-v) = c(H-σv), and degree reconstructibility identifies isolated vertices.
    • No isolated vertices: find a non-cut vertex w₀ (exists in every component of a graph with no isolated vertices) whose removal preserves the component count. Then c(G) = c(G-w₀) = c(H-σw₀) ≥ c(H) and symmetrically.