Kocay-Style Cover Counting

This module starts a typed version of the Kocay cover-counting machinery. The fully classical statement groups covers by isomorphism type of the covered subgraph. Here we first group finite indexed tuples of induced copies by their actual covered vertex set inside a fixed host graph.

This is the finite bookkeeping core behind Kocay-style linear constraints.

Main definitions

• SimpleGraph.coverFinset — finite indexed tuples of induced copies whose vertex-set union is a fixed U.
• SimpleGraph.coverCount — the number of such finite indexed covers.
• SimpleGraph.coverTypeCount — Kocay's target cover number: covers of all vertices of a target graph X.
• SimpleGraph.InducedSetIsoClass — isomorphism classes of induced subgraphs appearing as vertex subsets of a fixed host graph.
• SimpleGraph.coverCount_sum — the product of the indexed subgraph counts is the sum of cover counts over covered vertex sets.
• SimpleGraph.pairCoverFinset — ordered pairs of induced copies of F₁ and F₂ whose vertex-set union is a fixed U.
• SimpleGraph.pairCoverCount — the number of such ordered covers.
• SimpleGraph.pairCoverTypeCount — the two-pattern target cover number.

Main results

• SimpleGraph.coverTypeCount_sum_induce — the finite-index cover identity grouped by the actual induced target graph G[U].
• SimpleGraph.coverTypeCount_sum_inducedIsoClass — the finite-index cover identity grouped by induced-subgraph isomorphism classes: ∏ i s(Fᵢ,G) = ∑_X c((Fᵢ),X) * s(X,G) in typed quotient form.
• SimpleGraph.pairCoverCount_sum — the product subgraphCount F₁ G * subgraphCount F₂ G is the sum of these cover counts over all vertex subsets U.
• SimpleGraph.pairCoverTypeCount_sum_induce — the same ordered-pair identity grouped by the actual induced target graph G[U].
• SimpleGraph.SameDeck.subgraphCount_prod_eq — finite indexed products of Kelly-reconstructible subgraph counts are reconstructible.
• SimpleGraph.SameDeck.subgraphCount_mul_eq — products of reconstructible subgraph counts are reconstructible.

References

• Kocay, W. L. (1981). "Some new methods in reconstruction theory".

Finite indexed cover tuples

def SimpleGraph.coverUnion {V : Type u_3} [DecidableEq V] {ι : Type u_4} [Fintype ι] (S : ι → Finset V) : Finset V

The vertex set covered by an indexed tuple of copies.

Equations

• SimpleGraph.coverUnion S = Finset.univ.biUnion S

def SimpleGraph.coverFinset {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) (U : Finset V) : Finset (ι → Finset V)

Finite indexed tuples of induced copies of the patterns F i whose vertex-set union is U.

This is the typed, in-host cover object behind Kocay's lemma. The later isomorphism-type grouping should quotient or regroup these covers by the graph induced on U; this definition deliberately keeps the first finite bookkeeping layer concrete.

Equations

• SimpleGraph.coverFinset F G U = {S ∈ Fintype.piFinset fun (i : ι) => (F i).copyFinset G | SimpleGraph.coverUnion S = U}

def SimpleGraph.coverCount {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) (U : Finset V) : ℕ

The number of finite indexed covers of U by induced copies of F i.

Equations

• SimpleGraph.coverCount F G U = (SimpleGraph.coverFinset F G U).card

def SimpleGraph.coverTypeFinset {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] {X : Type u_6} [Fintype X] [DecidableEq X] (F : (i : ι) → SimpleGraph (W i)) (XG : SimpleGraph X) : Finset (ι → Finset X)

Kocay's target cover finset C((F_i), X): indexed induced copies of the patterns F i in the target graph XG whose union covers every vertex of XG.

Equations

• SimpleGraph.coverTypeFinset F XG = SimpleGraph.coverFinset F XG Finset.univ

def SimpleGraph.coverTypeCount {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] {X : Type u_6} [Fintype X] [DecidableEq X] (F : (i : ι) → SimpleGraph (W i)) (XG : SimpleGraph X) : ℕ

Kocay's target cover number c((F_i), X): the number of indexed induced copies of F i that cover all vertices of the target graph XG.

Equations

• SimpleGraph.coverTypeCount F XG = (SimpleGraph.coverTypeFinset F XG).card

@[simp]

theorem SimpleGraph.coverTypeCount_eq_coverCount_univ {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] {X : Type u_6} [Fintype X] [DecidableEq X] (F : (i : ι) → SimpleGraph (W i)) (XG : SimpleGraph X) : coverTypeCount F XG = coverCount F XG Finset.univ

theorem SimpleGraph.coverCount_sum {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) : ∏ i : ι, (F i).subgraphCount G = ∑ U ∈ Finset.univ.powerset, coverCount F G U

The finite indexed Kocay bookkeeping identity, grouped by the actual covered vertex set in the host graph.

The left side counts tuples of induced copies independently. The right side classifies the same tuples by the union of their vertex sets.

Target-cover counts up to isomorphism

theorem SimpleGraph.coverTypeCount_eq_of_iso {ι : Type u_4} [Fintype ι] [DecidableEq ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] {X : Type u_6} {Y : Type u_7} [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y] {XG : SimpleGraph X} {YG : SimpleGraph Y} (F : (i : ι) → SimpleGraph (W i)) (φ : XG ≃g YG) : coverTypeCount F XG = coverTypeCount F YG

Target-cover counts depend only on the isomorphism type of the target graph. This is the well-definedness bridge needed to group Kocay covers by isomorphism class rather than by concrete vertex subsets.

Ordered two-pattern cover tuples

def SimpleGraph.pairCoverFinset {W₁ : Type u_1} {W₂ : Type u_2} {V : Type u_3} [Fintype W₁] [Fintype W₂] [Fintype V] [DecidableEq V] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (G : SimpleGraph V) (U : Finset V) : Finset (Finset V × Finset V)

Ordered pairs of induced copies of F₁ and F₂ whose vertex-set union is U. This is a typed, in-host version of the cover tuples appearing in Kocay's lemma.

Equations

• F₁.pairCoverFinset F₂ G U = {p ∈ (F₁.copyFinset G).product (F₂.copyFinset G) | p.1 ∪ p.2 = U}

def SimpleGraph.pairCoverCount {W₁ : Type u_1} {W₂ : Type u_2} {V : Type u_3} [Fintype W₁] [Fintype W₂] [Fintype V] [DecidableEq V] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (G : SimpleGraph V) (U : Finset V) : ℕ

The number of ordered pairs of induced copies of F₁ and F₂ covering the vertex set U.

Equations

• F₁.pairCoverCount F₂ G U = (F₁.pairCoverFinset F₂ G U).card

def SimpleGraph.pairCoverTypeFinset {W₁ : Type u_1} {W₂ : Type u_2} [Fintype W₁] [Fintype W₂] {X : Type u_4} [Fintype X] [DecidableEq X] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (XG : SimpleGraph X) : Finset (Finset X × Finset X)

Ordered pairs of induced copies in the target graph XG covering every vertex of XG.

Equations

• F₁.pairCoverTypeFinset F₂ XG = F₁.pairCoverFinset F₂ XG Finset.univ

def SimpleGraph.pairCoverTypeCount {W₁ : Type u_1} {W₂ : Type u_2} [Fintype W₁] [Fintype W₂] {X : Type u_4} [Fintype X] [DecidableEq X] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (XG : SimpleGraph X) : ℕ

The ordered two-pattern target cover number c((F₁, F₂), X).

Equations

• F₁.pairCoverTypeCount F₂ XG = (F₁.pairCoverTypeFinset F₂ XG).card

@[simp]

theorem SimpleGraph.pairCoverTypeCount_eq_pairCoverCount_univ {W₁ : Type u_1} {W₂ : Type u_2} [Fintype W₁] [Fintype W₂] {X : Type u_4} [Fintype X] [DecidableEq X] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (XG : SimpleGraph X) : F₁.pairCoverTypeCount F₂ XG = F₁.pairCoverCount F₂ XG Finset.univ

theorem SimpleGraph.coverCount_eq_coverTypeCount_induce {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {W : ι → Type u_6} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) (U : Finset V) : coverCount F G U = coverTypeCount F (induce (↑U) G)

Counting indexed covers of a concrete vertex set U in G is the same as counting target covers of the induced graph G[U].

theorem SimpleGraph.coverTypeCount_sum_induce {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {W : ι → Type u_6} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) : ∏ i : ι, (F i).subgraphCount G = ∑ U ∈ Finset.univ.powerset, coverTypeCount F (induce (↑U) G)

Finite-index Kocay bookkeeping grouped by the actual induced target graph on each covered vertex set.

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

Pattern isomorphism preserves induced-subgraph counts in a fixed host.

def SimpleGraph.InducedSetIsoRel {V : Type u_3} (G : SimpleGraph V) : Finset V → Finset V → Prop

Vertex subsets of a host graph are equivalent when they induce isomorphic subgraphs.

Equations

• G.InducedSetIsoRel U U' = Nonempty (SimpleGraph.induce (↑U) G ≃g SimpleGraph.induce (↑U') G)

def SimpleGraph.InducedSetIsoSetoid {V : Type u_3} (G : SimpleGraph V) : Setoid (Finset V)

The setoid on vertex subsets generated by induced-subgraph isomorphism.

Equations

• G.InducedSetIsoSetoid = { r := G.InducedSetIsoRel, iseqv := ⋯ }

@[reducible, inline]

abbrev SimpleGraph.InducedSetIsoClass {V : Type u_3} (G : SimpleGraph V) : Type u_3

Isomorphism classes of induced subgraphs appearing as vertex subsets of G.

Equations

• G.InducedSetIsoClass = Quotient G.InducedSetIsoSetoid

noncomputable instance SimpleGraph.inducedSetIsoClassFintype {V : Type u_3} [Fintype V] (G : SimpleGraph V) : Fintype G.InducedSetIsoClass

Equations

• G.inducedSetIsoClassFintype = Fintype.ofFinite G.InducedSetIsoClass

def SimpleGraph.inducedSetIsoClassOf {V : Type u_3} (G : SimpleGraph V) (U : Finset V) : G.InducedSetIsoClass

The induced-subgraph isomorphism class of a concrete vertex subset.

Equations

• G.inducedSetIsoClassOf U = ⟦U⟧

noncomputable def SimpleGraph.inducedClassCoverTypeCount {V : Type u_3} [DecidableEq V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {W : ι → Type u_6} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) (q : G.InducedSetIsoClass) : ℕ

The Kocay cover number attached to an induced-subgraph isomorphism class.

Equations

• SimpleGraph.inducedClassCoverTypeCount F G q = Quotient.lift (fun (U : Finset V) => SimpleGraph.coverTypeCount F (SimpleGraph.induce (↑U) G)) ⋯ q

noncomputable def SimpleGraph.inducedClassSubgraphCount {V : Type u_3} [Fintype V] (G : SimpleGraph V) (q : G.InducedSetIsoClass) : ℕ

The number of induced copies in G of an induced-subgraph isomorphism class.

Equations

• G.inducedClassSubgraphCount q = Quotient.lift (fun (U : Finset V) => (SimpleGraph.induce (↑U) G).subgraphCount G) ⋯ q

theorem SimpleGraph.inducedSetIsoClass_fiber_card {V : Type u_3} [Fintype V] (G : SimpleGraph V) (q : G.InducedSetIsoClass) : {U ∈ Finset.univ.powerset | G.inducedSetIsoClassOf U = q}.card = G.inducedClassSubgraphCount q

theorem SimpleGraph.coverTypeCount_sum_inducedIsoClass {V : Type u_3} [Fintype V] [DecidableEq V] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {W : ι → Type u_6} [(i : ι) → Fintype (W i)] (F : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) : ∏ i : ι, (F i).subgraphCount G = ∑ q : G.InducedSetIsoClass, inducedClassCoverTypeCount F G q * G.inducedClassSubgraphCount q

Kocay's finite product-count identity, grouped by induced-subgraph isomorphism classes. This is the typed quotient form of ∏ i s(Fᵢ, G) = ∑_X c((Fᵢ), X) * s(X, G): the quotient ranges over the isomorphism classes of induced subgraphs actually appearing in the host.

theorem SimpleGraph.pairCoverCount_eq_pairCoverTypeCount_induce {W₁ : Type u_1} {W₂ : Type u_2} {V : Type u_3} [Fintype W₁] [Fintype W₂] [Fintype V] [DecidableEq V] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (G : SimpleGraph V) (U : Finset V) : F₁.pairCoverCount F₂ G U = F₁.pairCoverTypeCount F₂ (induce (↑U) G)

Counting ordered covers of a concrete vertex set U in G is the same as counting ordered target covers of the induced graph G[U].

theorem SimpleGraph.pairCoverCount_sum {W₁ : Type u_1} {W₂ : Type u_2} {V : Type u_3} [Fintype W₁] [Fintype W₂] [Fintype V] [DecidableEq V] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (G : SimpleGraph V) : F₁.subgraphCount G * F₂.subgraphCount G = ∑ U ∈ Finset.univ.powerset, F₁.pairCoverCount F₂ G U

The ordered-pair Kocay bookkeeping identity, grouped by covered vertex set.

theorem SimpleGraph.pairCoverTypeCount_sum_induce {W₁ : Type u_1} {W₂ : Type u_2} {V : Type u_3} [Fintype W₁] [Fintype W₂] [Fintype V] [DecidableEq V] (F₁ : SimpleGraph W₁) (F₂ : SimpleGraph W₂) (G : SimpleGraph V) : F₁.subgraphCount G * F₂.subgraphCount G = ∑ U ∈ Finset.univ.powerset, F₁.pairCoverTypeCount F₂ (induce (↑U) G)

Ordered two-pattern cover identity grouped by the actual induced target graph on each covered vertex set.

theorem SimpleGraph.SameDeck.subgraphCount_prod_eq {V : Type u_3} [Fintype V] {G H : SimpleGraph V} {ι : Type u_4} [Fintype ι] {W : ι → Type u_5} [(i : ι) → Fintype (W i)] (h : G.SameDeck H) (F : (i : ι) → SimpleGraph (W i)) (hcard : ∀ (i : ι), Fintype.card (W i) < Fintype.card V) : ∏ i : ι, (F i).subgraphCount G = ∏ i : ι, (F i).subgraphCount H

Finite indexed products of reconstructible induced-subgraph counts are reconstructible. This is the product side of the finite-index Kocay identity.

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

Products of reconstructible induced-subgraph counts are reconstructible. This is the simplest Kocay-style linear constraint supplied by Kelly's lemma.