Homomorphism counts into a lexicographic product

Lax871432.LexicographicProductCounts · concepts/Lax871432/LexicographicProductCounts.lean · lax-871432

proven

Loading review…

For simple graphs $F$ , $G$ and $H$ ,

\hom(F, G \cdot H) = \sum_{\mathcal{R}} \hom(F / \mathcal{R}, G) \hom(\textstyle\coprod_{R \in \mathcal{R}} F[R], H),

the sum ranging over the partitions $\mathcal{R}$ of $V(F)$ all of whose classes induce connected subgraphs.

Concept map

4 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

1	import Mathlib.Algebra.BigOperators.Ring.Finset
2	import Lax871432.ConnectedPartitions
3	import Lax871432.GraphProducts
4	import Lax871432.HomomorphismCounts
5
6	/-!
7	---
8	title: Homomorphism counts into a lexicographic product
9	type: theorem
10	---
11	For simple graphs $F$ , $G$ and $H$ ,
12	$\hom(F, G \cdot H) = \sum_{\mathcal{R}} \hom(F / \mathcal{R}, G) \hom(\textstyle\coprod_{R \in \mathcal{R}} F[R], H),$
13
14	the sum ranging over the partitions $\mathcal{R}$ of $V(F)$ all of whose classes induce
15	connected subgraphs.
16	-/
17
18	open Lax871432.ConnectedPartitions Lax871432.GraphProducts Lax871432.HomomorphismCounts
19
20	namespace Lax871432.LexicographicProductCounts
21
22	/-- Homomorphisms into a lexicographic product: they are counted by the partitions of the
23	source into connected parts, a homomorphism from the quotient into the left factor and a
24	homomorphism from the disjoint union of the parts into the right factor. -/
25	axiom homCount_lexProd {U V W : Type*} [Finite U] [Finite V] [Finite W] (F : SimpleGraph U)
26	(G : SimpleGraph V) (H : SimpleGraph W) :
27	homCount F (lexProd G H) =
28	∑ 𝓡 : ConnPart F, homCount 𝓡.quotientGraph G * homCount 𝓡.parts H
29
30	end Lax871432.LexicographicProductCounts
31

Builds on

Used by

none

From Mathlib

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive