Kelly's Lemma (Subgraph Counting)

Kelly's Lemma is the central counting tool in reconstruction theory. It states that for any graph F with fewer vertices than G, the number of induced copies of F in G is reconstructible from the deck.

Main definitions

• SimpleGraph.copyFinset — the set of k-element subsets S ⊆ V(G) whose induced subgraph G[S] is isomorphic to F
• SimpleGraph.subgraphCount — |copyFinset F G|, the number of such copies

Main results

• SimpleGraph.subgraphCount_sum — the double-counting identity: (n - k) * s(F, G) = ∑ v, s(F, G - v)
• SimpleGraph.SameDeck.subgraphCount_eq — if deck(G) = deck(H) and |V(F)| < |V(G)|, then s(F, G) = s(F, H)

References

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

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

The set of Fintype.card W-element subsets S ⊆ V whose induced subgraph G[S] is isomorphic to F.

Equations

• F.copyFinset G = {S ∈ Finset.powersetCard (Fintype.card W) Finset.univ | Nonempty (SimpleGraph.induce (↑S) G ≃g F)}

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

The number of induced copies of F in G: how many k-element subsets S ⊆ V(G) satisfy G[S] ≅ F.

Equations

• F.subgraphCount G = (F.copyFinset G).card

theorem SimpleGraph.mem_copyFinset {W : Type u_1} [Fintype W] {V : Type u_2} [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) (S : Finset V) : S ∈ F.copyFinset G ↔ S.card = Fintype.card W ∧ Nonempty (induce (↑S) G ≃g F)

theorem SimpleGraph.copyFinset_card {W : Type u_1} [Fintype W] {V : Type u_2} [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) {S : Finset V} (hS : S ∈ F.copyFinset G) : S.card = Fintype.card W

Every set in copyFinset F G has cardinality Fintype.card W.

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

subgraphCount is invariant under graph isomorphism.

theorem SimpleGraph.subgraphCount_deleteVert {W : Type u_1} [Fintype W] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph W) (G : SimpleGraph V) (v : V) : F.subgraphCount (G.deleteVert v) = {S ∈ F.copyFinset G | v ∉ S}.card

Bridge lemma: copies of F in G - v biject with copies of F in G that avoid v.

theorem SimpleGraph.subgraphCount_sum {W : Type u_1} [Fintype W] {V : Type u_2} [Fintype V] (F : SimpleGraph W) (G : SimpleGraph V) [DecidableEq V] (_hcard : Fintype.card W ≤ Fintype.card V) : (Fintype.card V - Fintype.card W) * F.subgraphCount G = ∑ v : V, F.subgraphCount (G.deleteVert v)

Kelly's counting identity (double-counting). For any graph F on k vertices and G on n ≥ k vertices: (n - k) * s(F, G) = ∑ v, s(F, G - v).

theorem SimpleGraph.SameDeck.subgraphCount_eq {W : Type u_1} [Fintype W] {V : Type u_2} [Fintype V] {G H : SimpleGraph V} (h : G.SameDeck H) (F : SimpleGraph W) (hcard : Fintype.card W < Fintype.card V) : F.subgraphCount G = F.subgraphCount H

Kelly's Lemma (reconstructibility corollary). If two graphs have the same deck and |V(F)| < |V(G)|, then they have the same number of induced copies of F.