Homomorphism counts into a looped graph

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

proven

Loading review…

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

\hom(F, G^\circ) = \sum_{L \subseteq E(F)} \hom(F \oslash L, G),

where $G^\circ$ carries a loop at every vertex and $F \oslash L$ is the contraction quotient of $F$ by the edge set $L$ .

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.Algebra.BigOperators.Ring.Finset
2	import Lax871432.LoopGraphs
3
4	/-!
5	---
6	title: Homomorphism counts into a looped graph
7	type: theorem
8	---
9	For finite simple graphs $F$ and $G$ ,
10	$\hom(F, G^\circ) = \sum_{L \subseteq E(F)} \hom(F \oslash L, G),$
11	where $G^\circ$ carries a loop at every vertex and $F \oslash L$ is the contraction quotient
12	of $F$ by the edge set $L$ .
13	-/
14
15	open Lax871432.LoopGraphs
16
17	open scoped Lax871432.LoopGraphs
18
19	namespace Lax871432.LoopedGraphCounts
20
21	/-- Homomorphisms into a looped graph: a homomorphism from `F` to `G°` is the same thing
22	as a set `L` of edges of `F`, those it collapses to loops, together with a homomorphism from
23	the contraction quotient `F ⊘ L` to `G`. -/
24	axiom homCount_looped {V W : Type*} [Finite V] [Finite W] (F : SimpleGraph V)
25	(G : SimpleGraph W) :
26	letI : Fintype F.edgeSet := Fintype.ofFinite _
27	LoopGraph.homCount (toLoopGraph F) (looped G) =
28	∑ L : Finset F.edgeSet, LoopGraph.homCount (F ⊘ (edgeSetOf F) L) (toLoopGraph G)
29
30	end Lax871432.LoopedGraphCounts
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