Homomorphism counts into a disjoint union

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

proven

Loading review…

For a connected simple graph $K$ and simple graphs $G_1$ and $G_2$ ,

\hom(K, G_1 + G_2) = \hom(K, G_1) + \hom(K, G_2),

where $G_1 + G_2$ denotes the disjoint union of $G_1$ and $G_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.Connectivity.Connected
2	import Mathlib.Combinatorics.SimpleGraph.Sum
3	import Lax871432.HomomorphismCounts
4
5	/-!
6	---
7	title: Homomorphism counts into a disjoint union
8	type: lemma
9	---
10	For a connected simple graph $K$ and simple graphs $G_1$ and $G_2$ ,
11	$\hom(K, G_1 + G_2) = \hom(K, G_1) + \hom(K, G_2),$
12	where $G_1 + G_2$ denotes the disjoint union of $G_1$ and $G_2$ .
13	-/
14
15	open Lax871432.HomomorphismCounts
16
17	namespace Lax871432.DisjointUnionCounts
18
19	/-- A homomorphism from a connected graph into a disjoint union maps into one of its two
20	parts. -/
21	axiom homCount_sum_right {U V W : Type*} [Finite U] [Finite V] [Finite W] (K : SimpleGraph U)
22	(hK : K.Connected) (G₁ : SimpleGraph V) (G₂ : SimpleGraph W) :
23	homCount K (G₁ ⊕g G₂) = homCount K G₁ + homCount K G₂
24
25	end Lax871432.DisjointUnionCounts
26

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