Component Counts and Subgraph Counts

This module develops the component-count ↔ subgraph-count machinery needed for Kelly's 1942 multiset-recovery induction in the reconstruction of disconnected graphs. The centerpiece is a decomposition identity: for any connected graph F, the number of induced copies of F in G equals the sum of induced copies of F in each connected component of G.

Main definitions

• SimpleGraph.componentCount — for a (connected) graph F and a graph G, the number of connected components of G whose induced subgraph is isomorphic to F.

Main results

• SimpleGraph.componentCount_eq_of_iso — component counts are iso-invariants.
• SimpleGraph.ConnectedComponent.card_supp_lt_of_not_connected — in a finite disconnected graph, every connected component has fewer vertices than the host.
• SimpleGraph.subgraphCount_eq_sum_over_components — if F is connected, subgraphCount F G = ∑ c, subgraphCount F (G.induce c.supp). This is the structural identity that lets the reconstruction induction turn subgraph counts (given by Kelly's Lemma) into component counts.
• SimpleGraph.subgraphCount_eq_componentCount_add_larger — the triangular accounting identity: copies of a connected F in G are the components isomorphic to F, plus copies lying inside strictly larger components.
• SimpleGraph.componentIsoClassEquivOfComponentCountEq — equal component counts for a fixed connected-component type give an equivalence between the corresponding component fibers.
• SimpleGraph.componentEquivOfComponentCountEq — equal component counts for every component type assemble into a global component bijection preserving component isomorphism classes.
• SimpleGraph.largerComponentEquivOfComponentCountEq — equal component counts for every component type above a size threshold assemble into the restricted larger-component matching used by the triangular induction.
• SimpleGraph.SameDeck.componentCount_eq_components_of_not_connected — the descending triangular induction recovering every represented component isomorphism class in two same-deck disconnected graphs.

References

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

def SimpleGraph.componentCount {W : Type u_1} {V : Type u_2} [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) : ℕ

The number of connected components of G whose induced subgraph G.induce c.supp is isomorphic to the reference graph F.

Equations

• F.componentCount G = Fintype.card { c : G.ConnectedComponent // Nonempty (SimpleGraph.induce c.supp G ≃g F) }

Component size in disconnected graphs

theorem SimpleGraph.connected_of_component_supp_eq_univ {V : Type u_2} {G : SimpleGraph V} (C : G.ConnectedComponent) (hC : C.supp = Set.univ) : G.Connected

If one connected component contains every vertex, then the graph is connected.

theorem SimpleGraph.ConnectedComponent.card_supp_lt_of_not_connected {V : Type u_2} [Fintype V] {G : SimpleGraph V} (hG : ¬G.Connected) (C : G.ConnectedComponent) : Fintype.card ↑C.supp < Fintype.card V

In a disconnected finite graph, every connected component is a proper vertex subset. In particular, component graphs are small enough for Kelly's Lemma whenever the host graph is disconnected.

Isomorphism invariance of componentCount

theorem SimpleGraph.componentCount_eq_of_iso {W : Type u_1} {V₁ : Type u_3} {V₂ : Type u_4} [Fintype V₁] [Fintype V₂] {G₁ : SimpleGraph V₁} {G₂ : SimpleGraph V₂} (F : SimpleGraph W) (φ : G₁ ≃g G₂) : F.componentCount G₁ = F.componentCount G₂

Component counts are invariant under graph isomorphism.

Small host and equal-size host counts

theorem SimpleGraph.subgraphCount_eq_zero_of_card_lt {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) (hcard : Fintype.card V < Fintype.card W) : F.subgraphCount G = 0

If the host graph has fewer vertices than F, then it has no induced copies of F.

theorem SimpleGraph.subgraphCount_eq_one_or_zero_of_card_eq {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) (hcard : Fintype.card W = Fintype.card V) : F.subgraphCount G = if Nonempty (G ≃g F) then 1 else 0

If the host graph and F have the same number of vertices, then the induced-copy count is all-or-nothing: it is 1 if the whole host is isomorphic to F, and 0 otherwise.

Component decomposition of subgraphCount

For F connected and G arbitrary, every copy of F in G sits inside a single connected component of G. We prove this and then show subgraphCount F G = ∑ c, subgraphCount F (G.induce c.supp).

theorem SimpleGraph.subgraphCount_eq_sum_over_components {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] (F : SimpleGraph W) (G : SimpleGraph V) (hF : F.Connected) : F.subgraphCount G = ∑ c : G.ConnectedComponent, F.subgraphCount (induce c.supp G)

Component decomposition for subgraph counts. If F is connected, the number of induced copies of F in G equals the sum, over connected components c of G, of the number of induced copies of F in the component-induced subgraph G.induce c.supp.

Triangular component-count accounting

theorem SimpleGraph.componentCount_eq_sum_ite {W : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph W) (G : SimpleGraph V) : F.componentCount G = ∑ c : G.ConnectedComponent, if Nonempty (induce c.supp G ≃g F) then 1 else 0

Component counts as a sum of indicator functions over connected components. This is the cardinality form used when separating equal-size components from larger components.

theorem SimpleGraph.componentCount_eq_sum_same_card_subgraphCount {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] (F : SimpleGraph W) (G : SimpleGraph V) : F.componentCount G = ∑ c : G.ConnectedComponent with Fintype.card ↑c.supp = Fintype.card W, F.subgraphCount (induce c.supp G)

On components with the same number of vertices as F, the induced-copy sum is exactly the component count for F.

theorem SimpleGraph.subgraphCount_eq_componentCount_add_larger {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] (F : SimpleGraph W) (G : SimpleGraph V) (hF : F.Connected) : F.subgraphCount G = F.componentCount G + ∑ c : G.ConnectedComponent with Fintype.card W < Fintype.card ↑c.supp, F.subgraphCount (induce c.supp G)

Triangular component-count accounting. If F is connected, then every induced copy of F in G is either an entire connected component isomorphic to F, or it lies inside a strictly larger connected component. This identity is the bookkeeping step behind Kelly's disconnected-graph reconstruction induction.

theorem SimpleGraph.largerComponentSubgraphCount_sum_eq_of_isoEquiv {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] {G H : SimpleGraph V} (F : SimpleGraph W) (e : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp } ≃ { c : H.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }) (hiso : ∀ (c : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }), Nonempty (induce (↑c).supp G ≃g induce (↑(e c)).supp H)) : ∑ c : G.ConnectedComponent with Fintype.card W < Fintype.card ↑c.supp, F.subgraphCount (induce c.supp G) = ∑ c : H.ConnectedComponent with Fintype.card W < Fintype.card ↑c.supp, F.subgraphCount (induce c.supp H)

If the strictly larger components of G and H can be paired by isomorphism, then they make the same contribution to the triangular component-count identity for F.

This is the bookkeeping form of the induction hypothesis in Kelly's component-multiset recovery: once all components larger than F have been matched by isomorphism, the larger-component error term is known to agree.

theorem SimpleGraph.SameDeck.componentCount_eq_of_larger_sum_eq {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] {G H : SimpleGraph V} (h : G.SameDeck H) (F : SimpleGraph W) (hF : F.Connected) (hcard : Fintype.card W < Fintype.card V) (hlarger : ∑ c : G.ConnectedComponent with Fintype.card W < Fintype.card ↑c.supp, F.subgraphCount (induce c.supp G) = ∑ c : H.ConnectedComponent with Fintype.card W < Fintype.card ↑c.supp, F.subgraphCount (induce c.supp H)) : F.componentCount G = F.componentCount H

The cancellative step for the disconnected-graph induction. If the strictly-larger-component contribution for a connected graph F is already known to agree for two same-deck graphs, then the number of connected components isomorphic to F agrees as well.

theorem SimpleGraph.SameDeck.componentCount_eq_of_larger_component_isoEquiv {W : Type u_1} {V : Type u_2} [Fintype W] [Fintype V] [DecidableEq V] {G H : SimpleGraph V} (h : G.SameDeck H) (F : SimpleGraph W) (hF : F.Connected) (hcard : Fintype.card W < Fintype.card V) (e : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp } ≃ { c : H.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }) (hiso : ∀ (c : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }), Nonempty (induce (↑c).supp G ≃g induce (↑(e c)).supp H)) : F.componentCount G = F.componentCount H

The local triangular induction step for component-multiset recovery.

For a connected graph F with fewer vertices than the host graphs, suppose that all strictly larger components of G and H have already been paired by isomorphism. Then the number of connected components isomorphic to F agrees between G and H.

The next few private definitions build a common quotient of the connected components of G and H by component-graph isomorphism. The public theorem below then uses fiberwise cardinal equality over this quotient to assemble a global component matching.

noncomputable def SimpleGraph.componentEquivOfComponentCountEq {V : Type u_2} [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) : G.ConnectedComponent ≃ H.ConnectedComponent

Equal component counts for every component isomorphism class assemble into a global bijection between the connected components of G and H.

Equations

• SimpleGraph.componentEquivOfComponentCountEq hGcount hHcount = Equiv.ofFiberEquiv (SimpleGraph.componentIsoClassFiberEquiv✝ hGcount hHcount)

theorem SimpleGraph.componentEquivOfComponentCountEq_iso {V : Type u_2} [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) (c : G.ConnectedComponent) : Nonempty (induce c.supp G ≃g induce ((componentEquivOfComponentCountEq hGcount hHcount) c).supp H)

The component bijection obtained from per-class component-count equality preserves the component isomorphism class.

noncomputable def SimpleGraph.componentIsoClassEquivOfComponentCountEq {W : Type u_1} {V : Type u_2} [Fintype V] {G H : SimpleGraph V} (F : SimpleGraph W) (hcount : F.componentCount G = F.componentCount H) : { c : G.ConnectedComponent // Nonempty (induce c.supp G ≃g F) } ≃ { c : H.ConnectedComponent // Nonempty (induce c.supp H ≃g F) }

Equal component counts for a fixed component type F produce a bijection between the components of G and H whose induced component graphs are isomorphic to F.

This packages the cardinal equality supplied by the triangular recovery step into the actual matching object needed for the later global assembly.

Equations

• SimpleGraph.componentIsoClassEquivOfComponentCountEq F hcount = Fintype.equivOfCardEq hcount

Matching components above a size threshold

The local triangular recovery step only needs an isomorphism-preserving matching between the components strictly larger than the current connected graph F. The following restricted version of the component-class matching API packages exactly that induction hypothesis.

noncomputable def SimpleGraph.largerComponentEquivOfComponentCountEq {V : Type u_2} [Fintype V] {G H : SimpleGraph V} {W : Type u_3} [Fintype W] (hGcount : ∀ (c : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }), (induce (↑c).supp G).componentCount G = (induce (↑c).supp G).componentCount H) (hHcount : ∀ (d : { d : H.ConnectedComponent // Fintype.card W < Fintype.card ↑d.supp }), (induce (↑d).supp H).componentCount G = (induce (↑d).supp H).componentCount H) : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp } ≃ { d : H.ConnectedComponent // Fintype.card W < Fintype.card ↑d.supp }

Equal component counts for every component above a size threshold assemble into a bijection between the larger-component subtypes.

Equations

• SimpleGraph.largerComponentEquivOfComponentCountEq hGcount hHcount = Equiv.ofFiberEquiv (SimpleGraph.largerComponentIsoClassFiberEquiv✝ hGcount hHcount)

theorem SimpleGraph.largerComponentEquivOfComponentCountEq_iso {V : Type u_2} [Fintype V] {G H : SimpleGraph V} {W : Type u_3} [Fintype W] (hGcount : ∀ (c : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }), (induce (↑c).supp G).componentCount G = (induce (↑c).supp G).componentCount H) (hHcount : ∀ (d : { d : H.ConnectedComponent // Fintype.card W < Fintype.card ↑d.supp }), (induce (↑d).supp H).componentCount G = (induce (↑d).supp H).componentCount H) (c : { c : G.ConnectedComponent // Fintype.card W < Fintype.card ↑c.supp }) : Nonempty (induce (↑c).supp G ≃g induce (↑((largerComponentEquivOfComponentCountEq hGcount hHcount) c)).supp H)

The larger-component bijection obtained from component-count equality preserves component isomorphism classes.

Descending recovery of represented component classes

theorem SimpleGraph.SameDeck.componentCount_eq_components_of_not_connected {V : Type u_2} [Fintype V] {G H : SimpleGraph V} (h : G.SameDeck H) (hGdisc : ¬G.Connected) (hHdisc : ¬H.Connected) : (∀ (c : G.ConnectedComponent), (induce c.supp G).componentCount G = (induce c.supp G).componentCount H) ∧ ∀ (d : H.ConnectedComponent), (induce d.supp H).componentCount G = (induce d.supp H).componentCount H

In two same-deck disconnected graphs, every component isomorphism class represented in either graph has the same multiplicity in both graphs.

This is the triangular induction in Kelly's disconnected-graph reconstruction argument. The induction descends by component size: for a component type F, Kelly's Lemma recovers the induced-subgraph count of F, and all strictly larger component contributions have already been matched by the induction hypothesis.