pathGraph coloring

Stream: graph theory

[Iván Renison]

Hello, I want to start contributing to mathlib, and I want to ask if defining a 2-coloring of pathGraph and proving that the chromatic number of pathGraph is 2 would be a good contribution?

[Kyle Miller]

Sure, seems good. I suggest that you use docs#SimpleGraph.Coloring.mk with a function Fin n -> Bool defined by maybe fun i => i.val % 2 == 0, and then you'll be able to use docs#SimpleGraph.Coloring.to_colorable to quickly get 2-colorability of docs#SimpleGraph.pathGraph

It should be straightforward to prove that the chromatic number is exactly two when the pathGraph has at least two vertices (i.e., when 2 <= n in pathGraph n). (Maybe use le_antisymm with SimpleGraph.chromaticNumber_le_of_colorable and prove the other case by contradiction.)

[Iván Renison]

Great! Thanks for the suggestions

[Iván Renison]

I have another question
In what file of mathlib I should put these new definition ans theorem?
In Mathlib.Combinatorics.SimpleGraph.Hasse it's okey?

[Kyle Miller]

These shouldn't go into Hasse. Maybe create a new file called ConcreteColorings? I'm not sure about the name.

[Iván Renison]

SimpleGraph.CompleteBipartiteGraph.bicoloring is in Mathlib.Combinatorics.SimpleGraph.Coloring, but it seems like something more general than these coloring, so I suppose that is a good idea to create a file ConcreteColorings

[Kyle Miller]

(Zulip trick: if you do docs#SimpleGraph.CompleteBipartiteGraph.bicoloring it creates a clickable link). We could move that coloring to your new file.

[Iván Renison]

Here I created the new file in a branch: https://github.com/leanprover-community/mathlib4/blob/IvanRenison_pathGraph_bicoloring/Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
For now only with the bicoloring of pathGraph

[Iván Renison]

I should make a pull request only with that very little change and add more things in other pull request, or I should add more things (the prof that the chromatic number is two) first?

[Kyle Miller]

Usually refactorings should be in their own PRs, but if you have a larger PR creating ConcreteColorings that incidentally moves this one definition, I'm happy to review it in this case. If you want, you can do it in two PRs.

[Iván Renison]

I have just opened the pull request
I will be happy to make changes, because I'm still not to good with lean, so the code is not to nice