countable De Bruijn–Erdős theorem

Stream: maths

[Kyle Miller]

Greetings from the Berkeley Lean Seminar, where a bunch of us are learning Lean this summer. As my first "real" project, I decided to formalize the Nash-Williams argument for the following version of the De Bruijn–Erdős theorem, that if a graph with countably many vertices has the property that every finite subgraph can be n-colored, then the graph can be n-colored. This involved proving a specialization of Kőnig's lemma, that the inverse limit of an ℕ-indexed family of nonempty finite sets is nonempty.

So, fresh off the presses, here it is:

Coloring statement: https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean#L347

Kőnig's lemma: https://github.com/kmill/lean-graphcoloring/blob/master/src/konig.lean#L153

The proofs are terrible, but, hey, it's proved. (While any hints to clean things up would be appreciated, I don't want to harm any of your eyes with its very hacky state. I feel like much of it was constructed through pure force of will.)

Many decisions were made for pedagogical reasons, to learn different parts of Lean. Probably a more straightforward proof would be for the full De Bruijn–Erdős theorem, using ultrafilters to construct a coloring from a choice of coloring for each finite subgraph. (That is, a compactness argument.)

[Johan Commelin]

@Kyle Miller Nice! We also wrote a bunch of graph colouring stuff on the hedetniemi branch. But it hasn't made it into mathlib master yet.

[Johan Commelin]

Are you planning to PR this to mathlib?

[Kenny Lau]

feature request: GUI for hedetniemi branch

[Johan Commelin]

Assigned to: @Kenny Lau :rofl: :oops: :stuck_out_tongue_wink:

[David Wärn]

Very nice! I agree that the full theorem might be easier to prove -- either using ultrafilters, or Tychonoff, or Zorn (consider the poset of partial colourings that can be extended to cover any finite subgraph).

[Kevin Buzzard]

I want to say that this follows from the compactness theorem from logic but I'm no expert in this area

[Patrick Massot]

Who hacked Kevin's Zulip account again?

[Patrick Massot]

We already had people posting type theory messages using his account and now logic?!

[David Wärn]

Yes, compactness theorem for propositional logic is basically same thing as Tychonoff for products of finite spaces

[Dave]

^This is not totally true. Tychonoff implies it, yes, but you only need Boolean prime ideal theorem (they are equivalent), which is weaker than choice and so weaker than Tychonoff.

[David Wärn]

Right, I'm saying it's equivalent to "product of finite spaces is compact", which is all you need for De Bruijn–Erdos

[Patrick Lutz]

@Kevin Buzzard Yes, there is a pretty straightforward proof using the compactness theorem for first order logic. That proof also works for uncountable graphs, unlike the Konig's lemma proof (but like the Tychonoff proof).

[Kyle Miller]

Johan Commelin said:

Are you planning to PR this to mathlib?

I'm willing to create PRs, but I'm not exactly sure what the criteria for inclusion is. I've at least now factored out and cleaned up some possibly useful results in mylist, myoption, and myfintype (https://github.com/kmill/lean-graphcoloring/tree/master/src). The proof of this specialization of Konig's lemma has also been cleaned up a bit.

[Johan Commelin]

@Kyle Miller The criteria for inclusion are: it should follow the style guidelines, and it should not be "crackpot". If you cook up a definition of boolalas and prove 10.000 lines of code about them, without any connection to the outside world... then we probably aren't very interested. (Clearly, this doesn't apply to whay you've done.)
Also, when you PR, expect to get 50 comments about how to improve things... they're meant to help you (-;

[Mario Carneiro]

I don't know, boolala sounds pretty interesting if there is that much to say about it

[Scott Morrison]

If it's "recognisably maths", it passes the interest criterion. :-)

[Mario Carneiro]

I've been wondering about whether to submit my formalization of the type theory of C to mathlib. It's definitely starting to rot but it's also very far removed from everything else currently in mathlib

[Johan Commelin]

Why don't you start a computer_science/ top-level directory?

[Johan Commelin]

You could always put it in archive/

[Kyle Miller]

After about a year almost exactly, mathlib now has a generalized version of Kőnig's lemma integrated into the category theory library: docs#nonempty_sections_of_fintype_inverse_system

At this rate, there will be a PR for the De Bruijn–Erdős theorem by June 2022 :smile:

[Adam Topaz]

Isn't this theorem true with J satisfying docs#category_theory.is_cofiltered ?

[Adam Topaz]

Hah! I just saw your comment @Kyle Miller

TODO: The theorem hold also in the case `{J : Type u} [category J] [is_cofiltered J]`.

[Kyle Miller]

@Adam Topaz Yeah, I would have liked this generalized version, but as far as I understood the entries on the Stacks project, you reduce to the directed order case and then relate the limit you get there to the original cofiltered limit. I wasn't sure how to organize this, so it's a TODO for now.

[Adam Topaz]

I think there is just a direct proof... I'll see if I can generalize

[Kyle Miller]

Not only would it be more general, but it should clean up the universe and instance wrangling. There were two conflicting instances: the small_category from the directed_order applied to the ulift of J, vs the category from the ulift of the small_category from the directed_order on J.

[Kyle Miller]

A [is_cofiltered J] : is_cofiltered (ulift J) instance would simplify this

[Adam Topaz]

@Kyle Miller I generalized this in the branch branch#koenig_generalize but it needs some golfing and some cleanup which I don't have time for right now.

[Adam Topaz]

The small_category J condition can probably be relaxed further to just category J

[Adam Topaz]

(Note that the small category condition is required to have a Top.limit_cone F in nonempty_limit_cone_of_compact_t2_inverse_system)

[Kyle Miller]

Thanks @Adam Topaz! That was a nice and clean generalization -- I had tried a direct proof, but the right notion of a partial section eluded me.

I've refactored things, updated documentation, and generalized the fintype version to category J.

[Kyle Miller]

The ulift.small_category instance seemed like it might be problematic, since it conflicts with the category_theory.ulift_category instance (different morphism types). I replaced it with something to lift a category to a universe where it's a small category:

def as_small (α : Type u) [category.{v} α] := ulift.{max u v} α

instance (α : Type u) [category.{v} α] : small_category (as_small α) :=
{ hom := λ X Y, ulift.{max u v} (X.down ⟶ Y.down),
  id := λ X, ⟨𝟙 _⟩,
  comp := λ X Y Z f g, ⟨f.down ≫ g.down⟩ }

Not sure if this makes sense to have, but it helped with the small_category to category generalization.

[Adam Topaz]

Yes, you're right about the ulift category instance. The as_small thing looks like a good solution. It should go somewhere in the category theory folder!

[Adam Topaz]

Maybe in category_theory/category/ulift?

[Adam Topaz]

Similarly the directed_order to is_(co)filtered instance (and its various variants) should probably go in category_theory/filtered. Do we want to add a codirected_order class?

[Kyle Miller]

Do you have any thoughts about having an abbreviation for Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y in category_theory/filtered? I was using a local abbreviation finite_diagram_arrow O for it, but an argument can be made that it doesn't need a name. (Pinging @Scott Morrison)

[Adam Topaz]

Hmmm... I don't know. TBH I only used it because it's the format needed for things like docs#category_theory.is_cofiltered.inf

[Kyle Miller]

@Adam Topaz I'd worry about duplicate code with directed and codirected orders, but at least for now there really aren't any theorems about directed orders. Given that there are both filtered and cofiltered categories already, it seems like it would make sense to add a codirected_order class (and I wouldn't mind dropping all the op's!).

[Adam Topaz]

I don't know if it makes sense to introduce an abbreviation for this Sigma type. Maybe @Scott Morrison has an opinion?

[Adam Topaz]

Do we have a directed_order instance given a semilattice_sup (we should!)? If so, these sort of instances in category_theory/filtered could be generalized

[Kyle Miller]

According to the mathlib docs, the only docs#directed_order instance is the one from a linear_order

[Adam Topaz]

Ah. Well, that's another missing instance then...

[Adam Topaz]

I don't have much experience working with docs#order_dual but working with opposites in category theory is annoying enough that I do think it could be useful to have a codirected order class

[Adam Topaz]

(I don't even know what the opposite order is called...)

[Reid Barton]

It's called $\ge$, you may have known this at one point.

[Kevin Buzzard]

Oh wow, I remember that ancient rune