Injective-Homomorphism Copy Counts are Reconstructible

Kelly's Lemma (Reconstruction.KellyLemma) reconstructs induced copy counts. The Tutte/Kocay programme (strategy note R1) needs the not-necessarily-induced copy counts: the number of subgraph copies of a pattern F, counted here as injective graph homomorphisms F →g G (which is the subgraph-copy count times |Aut F|, a constant of F). This module proves they are deck-reconstructible for patterns on < |V| vertices (SameDeck.injHomCount_eq):

• an injective homomorphism with |F|-element image lands in the induced subgraph on its image, giving the partition identity injHomCount F G = ∑_{|U| = |F|} injHomCount F (G[U]) (injHomCount_eq_sum_induce);
• the count into a target is a target-isomorphism invariant (injHomCount_eq_of_iso);
• regrouping by the isomorphism class of G[U] (the GraphIsoClass engine of Reconstruction.SupportCount) turns the sum into Kelly-weighted class sums (sum_injHomCount_induce_eq), and Kelly's Lemma finishes.

This is the "subgraph-copy counting layer" prerequisite for the disconnected-spanning-subgraph step of Tutte's theorem (checklist §4): for spanning patterns the same identity isolates the full-vertex-set summand, exactly as Reconstruction.KocayHost does for cover counts.

References

• Kelly, P. J. (1942). "On isometric transformations".
• Kocay, W. L. (1981). "Some new methods in reconstruction theory".

noncomputable instance SimpleGraph.instFintypeHom_reconstruction {V : Type u_1} [Fintype V] {W : Type u_2} [Fintype W] {F : SimpleGraph W} {G : SimpleGraph V} : Fintype (F →g G)

Graph homomorphisms from a finite graph into a finite graph form a finite type (they are determined by their underlying functions).

Equations

• SimpleGraph.instFintypeHom_reconstruction = Fintype.ofInjective (fun (f : F →g G) => ⇑f) ⋯

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

The number of injective homomorphism copies of F in G. This is |Aut F| times the number of subgraph copies of F, so its reconstructibility is equivalent to that of the subgraph-copy count.

Equations

• F.injHomCount G = Fintype.card { f : F →g G // Function.Injective ⇑f }

theorem SimpleGraph.injHomCount_eq_of_iso {V : Type u_1} [Fintype V] [DecidableEq V] {W : Type u_2} [Fintype W] {V₂ : Type u_3} [Fintype V₂] [DecidableEq V₂] (F : SimpleGraph W) {G₁ : SimpleGraph V} {G₂ : SimpleGraph V₂} (φ : G₁ ≃g G₂) : F.injHomCount G₁ = F.injHomCount G₂

injHomCount is invariant under isomorphisms of the target.

theorem SimpleGraph.injHomCount_eq_sum_induce {V : Type u_1} [Fintype V] [DecidableEq V] {W : Type u_2} [Fintype W] (F : SimpleGraph W) (G : SimpleGraph V) : F.injHomCount G = ∑ U ∈ Finset.powersetCard (Fintype.card W) Finset.univ, F.injHomCount (induce (↑U) G)

Partition by image. Every injective homomorphism copy of F lands in the induced subgraph on its (|F|-element) image, and conversely every injective homomorphism into some G[U] with |U| = |F| is such a copy.

theorem SimpleGraph.sum_injHomCount_induce_eq {V : Type u_1} [Fintype V] [DecidableEq V] {W : Type u_2} [Fintype W] (F : SimpleGraph W) {G : SimpleGraph V} (m : ℕ) : ∑ U ∈ Finset.powersetCard m Finset.univ, F.injHomCount (induce (↑U) G) = ∑ q : GraphIsoClass m, (Quotient.out q).subgraphCount G * F.injHomCount (Quotient.out q)

Regrouping by isomorphism class: the third instantiation of the GraphIsoClass pattern (after walk counts and cover counts).

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

Injective-homomorphism (subgraph-copy) counts are reconstructible for patterns on fewer vertices than the host. Together with Kelly's Lemma for induced copies, this completes the counting toolkit of reconstruction theory: induced counts, products (Kocay.lean), host cover counts (KocayHost.lean), and now arbitrary-copy counts.