## Stream: graph theory

### Topic: chromatic polynomial

#### Kyle Miller (Dec 22 2022 at 19:01):

Now that we have docs#simple_graph.connected_component, it's finally possible to write down the chromatic polynomial of a simple graph. To get things started, here's a WIP PR: #18003

I think the easiest way to prove that chromatic polynomials actually compute the number of colorings is to go by way of a special type of graph where there are two types of edges. These have their own notion of colorings, where edges of the first type are equality constraints (the incident vertices have the same color) and edges of the second type are inequality constraints (the incident vertices have different colors).

This is motivated by a version of the chromatic polynomial from statistical mechanics, the antiferromagnetic zero-temperature limit of the Q-states Potts model. The different edge types correspond to either (1) ferromagnetic or (2) antiferromagnetic bond strengths. Having two edge types also seems to be a good way to work with deletion/contraction of simple graphs.

#### Kyle Miller (Dec 22 2022 at 19:01):

I'm not sure I'll spend too much time on this in the short term, and I'd be happy to have some help!

#### Kyle Miller (Dec 22 2022 at 19:03):

One important lemma that would be appreciated is the statement that the chromatic polynomial (of a "del_contr") satisfies the deletion-contraction relation.

#### Kyle Miller (Dec 22 2022 at 19:14):

@Yaël Dillies I believe this is of interest to you for your LeanCamCombi project, if you want to help finish this off. :smile:

Tutte polynomials are still are a bit out, since we need more about graph nullity to be developed. (With my algebraic topology hat on I'd prefer to call it $b_1$.) This is what some current PRs about maximal trees that others are working on will lead to. There's also the small issue of the fact that there are many formulations of Tutte polynomials, all more-or-less equivalent, but there's one of them that I think has nicer properties, at least for the sorts of things I've been interested in.

#### Bhavik Mehta (Dec 22 2022 at 19:17):

Since the Tutte polynomial specialises to the chromatic polynomial by restricting one variable to 0, is it better to define that first, and have the chromatic polynomial as a special case? Or is there some other generality gained by doing it separately?

#### Kyle Miller (Dec 22 2022 at 19:19):

I think the main consideration is that there are too many Tutte polynomials (there's "the" Tutte polynomial, the dichromate polynomial, the dichromatic polynomial, and the partition function of the Q-states Potts model)

#### Kyle Miller (Dec 22 2022 at 19:20):

The secondary consideration is that the chromatic polynomial is a single-variable specialization with a nice-enough definition, so it seems harmless to just define it in its nice form and have lemmas connecting it to other graph polynomials later. The hardest part is the proof that it actually counts colorings, which you don't get "for free" from the Tutte polynomial.

#### Kyle Miller (Dec 22 2022 at 20:08):

I forgot to mention another consideration: chromatic polynomials work just fine for simple graphs (and multigraphs don't add anything interesting to the theory), but Tutte polynomials are better suited for multigraphs.

#### Yaël Dillies (Dec 22 2022 at 20:16):

Ahah, I was about to spend the evening defining it! Very nice!

#### Yaël Dillies (Dec 26 2022 at 11:49):

What's the status of the PR? Can we work on it?

#### Kyle Miller (Dec 26 2022 at 14:09):

I haven't done anything with this PR. Go ahead and work on it!

#### Kyle Miller (Dec 31 2022 at 18:31):

I've added another direction for a proof that might be easier (and it's my favorite proof that evaluating the chromatic polynomial gives the number of colorings). It's a big calc block, and I haven't filled in any of the proofs yet: https://github.com/leanprover-community/mathlib/blob/bab246f42e9459f4374379d426ce3e46251355ce/src/combinatorics/simple_graph/chromatic.lean#L32

Feel free to chip in if you're so inclined! #18003

#### Kyle Miller (Dec 31 2022 at 18:36):

It might make sense to add some more intermediate steps, but I tried to give enough so that a human could follow it.

I'll mention here that

    ... = ∑ (f : V → α), ∏ e in G.edge_finset,
(1 - sym2.lift ⟨λ v w, ite (v = w) 1 0, by { intros, simp_rw eq_comm }⟩ e) : _
... = ∑ (f : V → α), ∑ A in G.edge_finset.powerset, ∏ e in A,
(- sym2.lift ⟨λ v w, ite (v = w) 1 0, by { intros, simp_rw eq_comm }⟩ e) : _


is that general version of inclusion-exclusion that's for expanding a product of binomials.

i.e.,

$\prod_{x \in X} (a_x + b_x) = \sum_{A\subseteq X} \left(\prod_{x\in A} a_x\right)\left(\prod_{x\in X-A} b_x\right)$

#### Yaël Dillies (Dec 31 2022 at 19:07):

This is exactly docs#finset.sum_mul_sum

#### Kyle Miller (Jan 01 2023 at 19:29):

@Yaël Dillies Seems like you might have meant to link to docs#finset.prod_add

#### Yaël Dillies (Jan 01 2023 at 22:05):

Yes indeed!

Last updated: Aug 03 2023 at 10:10 UTC