Homomorphism polynomials

Lax461425.HomomorphismPolynomials · concepts/Lax461425/HomomorphismPolynomials.lean · lax-461425

definition

Loading review…

Natural Language Statement

Definition

A pattern is a finite bipartite multigraph $F$ with a fixed bipartition $A \uplus B$ , where parallel edges are allowed. It is given by the multiplicity $F(a, b) \in \mathbb{N}$ of the edge $ab$ for all $a \in A$ and $b \in B$ . Its vertex set is $V(F) = A \uplus B$ , and its edges are the pairs $ab$ with $F(a,b) > 0$ . For $n \in \mathbb{N}$ , the homomorphism polynomial of $F$ is

\hom_{F,n} = \sum_{\substack{h_A \colon A \to [n] \\ h_B \colon B \to [n]}} \prod_{ab \in E(F)} x_{h_A(a), h_B(b)} \in \mathbb{K}[\mathcal{X}_n],

where the product counts edges with multiplicity. On the bi-adjacency matrix of a bipartite graph, it counts the homomorphisms respecting the bipartitions.

Concept map

1 concept; 6 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.MvPolynomial.Basic
2
3	/-!
4	---
5	title: Homomorphism polynomials
6	type: definition
7	---
8	A pattern is a finite bipartite multigraph $F$ with a fixed bipartition $A \uplus B$ , where
9	parallel edges are allowed. It is given by the multiplicity $F(a, b) \in \mathbb{N}$ of the
10	edge $ab$ for all $a \in A$ and $b \in B$ . Its vertex set is $V(F) = A \uplus B$ , and its edges
11	are the pairs $ab$ with $F(a,b) > 0$ . For $n \in \mathbb{N}$ , the homomorphism polynomial of
12	$F$ is
13
14	$\hom_{F,n} = \sum_{\substack{h_A \colon A \to [n] \\ h_B \colon B \to [n]}} \prod_{ab \in E(F)} x_{h_A(a), h_B(b)} \in \mathbb{K}[\mathcal{X}_n],$
15
16
17	where the product counts edges with multiplicity. On the bi-adjacency matrix of a bipartite
18	graph, it counts the homomorphisms respecting the bipartitions.
19	-/
20
21	namespace Lax461425.HomomorphismPolynomials
22
23	/-- A finite bipartite multigraph with bipartition `A ⊎ B`. -/
24	structure Pattern where
25	/-- The left side of the bipartition. -/
26	A : Type
27	/-- The right side of the bipartition. -/
28	B : Type
29	[fintypeA : Fintype A]
30	[decEqA : DecidableEq A]
31	[fintypeB : Fintype B]
32	[decEqB : DecidableEq B]
33	/-- `mult a b` is the number of edges between `a` and `b`. -/
34	mult : A → B → ℕ
35
36	attribute [instance] Pattern.fintypeA Pattern.decEqA Pattern.fintypeB Pattern.decEqB
37
38	/-- The homomorphism polynomial `hom_{F,n}` in the variables `x_{i,j}` for `i, j ∈ [n]`. -/
39	noncomputable def hom (K : Type*) [CommSemiring K] (F : Pattern) (n : ℕ) :
40	MvPolynomial (Fin n × Fin n) K :=
41	∑ hA : F.A → Fin n, ∑ hB : F.B → Fin n, ∏ a, ∏ b, MvPolynomial.X (hA a, hB b) ^ F.mult a b
42
43	end Lax461425.HomomorphismPolynomials
44

Builds on

none

Used by

From Mathlib

Mathlib.Algebra.MvPolynomial.Basic

Discussion

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

Loading discussion…

Lax Lean Archive

Homomorphism polynomials

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments