Homomorphism counts into a full complement

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

proven

Loading review…

For a simple graph $F$ and a graph $X$ ,

\hom(F, \widehat{X}) = \sum_{S \subseteq E(F)} (-1)^{|S|} \hom(F_S, X),

where $F_S$ is the spanning subgraph of $F$ with edge set $S$ (Lovász, Large Networks and Graph Limits, equation (5.23)).

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 full complement
7	type: theorem
8	---
9	For a simple graph $F$ and a graph $X$ ,
10	$\hom(F, \widehat{X}) = \sum_{S \subseteq E(F)} (-1)^{\|S\|} \hom(F_S, X),$
11	where $F_S$ is the spanning subgraph of $F$ with edge set $S$ (Lovász, *Large Networks and
12	Graph Limits*, equation (5.23)).
13	-/
14
15	open Lax871432.LoopGraphs
16
17	namespace Lax871432.FullComplementCounts
18
19	/-- Homomorphisms into a full complement, Lovász's equation (5.23): by inclusion–exclusion
20	over the edges of `F`, the number of homomorphisms from `F` to the full complement of `X` is
21	the alternating sum, over the subsets `s` of `E(F)`, of the numbers of homomorphisms from the
22	spanning subgraph `F_s` to `X`. -/
23	axiom homCount_fullCompl {V W : Type*} [Finite V] [Finite W] (F : SimpleGraph V)
24	(X : LoopGraph W) :
25	letI : Fintype F.edgeSet := Fintype.ofFinite _
26	(LoopGraph.homCount (toLoopGraph F) X.fullCompl : ℤ) =
27	∑ s : Finset F.edgeSet, (-1 : ℤ) ^ s.card *
28	(LoopGraph.homCount (toLoopGraph ((spanningSubgraph F) ((edgeSetOf F) s))) X : ℤ)
29
30	end Lax871432.FullComplementCounts
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