Counting graph homomorphisms

Cardinality bounds for homomorphisms and injective homomorphisms between finite simple graphs. These compare graph homomorphism counts with all vertex maps and embeddings, enabling the normalization and estimates used for finite homomorphism densities.

Main results

• SimpleGraph.card_hom_le bounds homomorphisms by all vertex maps.
• SimpleGraph.card_injective_hom_le bounds injective homomorphisms by vertex embeddings.
• SimpleGraph.card_injective_hom_eq_sum_map_le counts injective homomorphisms by the vertex embeddings whose mapped graph lies below the target.
• SimpleGraph.card_hom_eq_card_adjPreservingMaps counts homomorphisms by the adjacency-preserving vertex maps.
• SimpleGraph.card_injective_hom_eq_labelledCopyCount identifies the number of injective homomorphisms with Mathlib's SimpleGraph.labelledCopyCount, so injective homomorphism counts and labelled copy counts are one counting convention, not two.

theorem SimpleGraph.card_hom_eq_card_adjPreservingMaps {V : Type u_1} {W : Type u_2} (F : SimpleGraph V) (G : SimpleGraph W) : Nat.card (F →g G) = Nat.card { ψ : V → W // ∀ (a b : V), F.Adj a b → G.Adj (ψ a) (ψ b) }

Homomorphisms and adjacency-preserving vertex maps are counted alike.

theorem SimpleGraph.card_hom_le {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) : Nat.card (F →g G) ≤ Fintype.card W ^ Fintype.card V

The number of homomorphisms from F to G is bounded by the number of vertex maps.

theorem SimpleGraph.card_injective_hom_le {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) : Nat.card { φ : F →g G // Function.Injective ⇑φ } ≤ (Fintype.card W).descFactorial (Fintype.card V)

The number of injective homomorphisms from F to G is bounded by the number of embeddings of the vertex types.

theorem SimpleGraph.card_injective_hom_eq_labelledCopyCount {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) : Nat.card { φ : F →g G // Function.Injective ⇑φ } = G.labelledCopyCount F

The number of injective homomorphisms from F to G is Mathlib's labelled copy count.

SimpleGraph.Copy F G is definitionally an injective homomorphism, so this is an equivalence of subtypes. Mathlib takes the host graph first: G.labelledCopyCount F counts copies of F inside G.

Deliberately not @[simp]: the left-hand side is not in simp normal form, since Nat.card of a Fintype rewrites to Fintype.card.

theorem SimpleGraph.card_injective_hom_eq_sum_map_le {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) : Nat.card { φ : F →g G // Function.Injective ⇑φ } = ∑ f : V ↪ W, if SimpleGraph.map (⇑f) F ≤ G then 1 else 0

Injective graph homomorphisms are counted by the vertex embeddings whose mapped graph lies below the host graph.