Homomorphism counts from a disjoint union

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

proven

Loading review…

For simple graphs $F_1$ , $F_2$ and $G$ ,

\hom(F_1 + F_2, G) = \hom(F_1, G) \hom(F_2, G),

where $F_1 + F_2$ denotes the disjoint union of $F_1$ and $F_2$ .

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

1	import Mathlib.Combinatorics.SimpleGraph.Sum
2	import Lax871432.HomomorphismCounts
3
4	/-!
5	---
6	title: Homomorphism counts from a disjoint union
7	type: lemma
8	---
9	For simple graphs $F_1$ , $F_2$ and $G$ ,
10	$\hom(F_1 + F_2, G) = \hom(F_1, G) \hom(F_2, G),$
11	where $F_1 + F_2$ denotes the disjoint union of $F_1$ and $F_2$ .
12	-/
13
14	open Lax871432.HomomorphismCounts
15
16	namespace Lax871432.CoproductCounts
17
18	/-- A homomorphism from a disjoint union is a pair of homomorphisms from its two parts. -/
19	axiom homCount_sum_left {U V W : Type*} [Finite U] [Finite V] [Finite W] (F₁ : SimpleGraph U)
20	(F₂ : SimpleGraph V) (G : SimpleGraph W) :
21	homCount (F₁ ⊕g F₂) G = homCount F₁ G * homCount F₂ G
22
23	end Lax871432.CoproductCounts
24

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