Coloring odd loops / components

Stream: graph theory

[John Talbot]

Is this in Mathlib?

G.Colorable 2 ↔ ∀ u, ∀ (w : G.Walk u u), ¬ Odd w.length

I can see Walk.three_le_chromaticNumber_of_odd_loop but the other direction would seem to require something like

G.Colorable n ↔ ∀ c : G.ConnectedComponent, (G.induce c).Colorable n

which I also can't see.

Am I missing something obvious? (If not I'd be happy to add these.)

[Iván Renison]

I think those are not in Mathlib

[Iván Renison]

I agree in that something like that is needed for the other direction

[Iván Renison]

In #22085 I'm giving the name ConnectedComponent.toSimpleGraph to G.induce C.supp with the idea that it may help

[John Talbot]

Thanks for confirming!

So the way I'm doing this in #24546 is via Subgraph and in particular this lemma

lemma connected_induce_iff {s : Set V} :
    (G.induce s).Connected ↔ ((⊤ : G.Subgraph).induce s).Connected

It seems there is quite a lot developed for connectedness of G.induce s that goes via this Subgraph route, but we probably also want your ConnectedComponent.toSimpleGraph.