chromatic polynomial

Stream: graph theory

[Kyle Miller]

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]

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]

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]

@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]

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]

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]

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]

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]

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

[Yaël Dillies]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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]

This is exactly docs#finset.sum_mul_sum

[Kyle Miller]

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

[Yaël Dillies]

Yes indeed!